Bounded Model Checking for Parametric Timed Automata

DOI10.1007/978-3-642-29072-5_6MaRDI QIDQ2889614zbMATH OpenOpenAlexFDO

Authors Michał Knapik, Wojciech Penczek

Publication date 8 June 2012

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-29072-5_6

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Bounded model checking for timed automata
• scientific article; zbMATH DE number 1973987
• Durations and parametric model-checking in timed automata
• scientific article; zbMATH DE number 1701759
• Linear parametric model checking of timed automata
• SAT based bounded model checking with partial order semantics for timed automata
• Verified model checking of timed automata
• Formal Modeling and Analysis of Timed Systems
• Checking MTL Properties of Discrete Timed Automata via Bounded Model Checking
• Parameterised model checking for alternating-time temporal logic

Cited in

(34)

• scientific article; zbMATH DE number 7577576 (Why is no real title available?)
• Real-Time Model-Checking: Parameters everywhere
• \textsf{IMITATOR} 3: synthesis of timing parameters beyond decidability
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Bounded model checking for knowledge and real time
• Parametric multisingular hybrid Petri nets: formal definitions and analysis techniques
• Formal Modeling and Analysis of Timed Systems
• Linear parametric model checking of timed automata
• An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking
• Learning-based compositional parameter synthesis for event-recording automata
• Iterative bounded synthesis for efficient cycle detection in parametric timed automata
• What's decidable about parametric timed automata?
• Parameter synthesis for probabilistic timed automata using stochastic game abstractions
• Distributed parametric model checking timed automata under non-zenoness assumption
• Checking MTL Properties of Discrete Timed Automata via Bounded Model Checking
• On clock-aware LTL parameter synthesis of timed automata
• Timed automata relaxation for reachability
• Hypervolume Approximation in Timed Automata Model Checking
• LTL parameter synthesis of parametric timed automata
• A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets
• Parametric Deadlock-Freeness Checking Timed Automata
• Cycle encoding-based parameter synthesis for timed automata safety
• Parametric Timed Model Checking for Guaranteeing Timed Opacity
• Bounded parametric verification for distributed time Petri nets with discrete-time semantics
• Integer-complete synthesis for bounded parametric timed automata
• scientific article; zbMATH DE number 1852149 (Why is no real title available?)
• Parameter synthesis for hierarchical concurrent real-time systems
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Formal Modeling and Analysis of Timed Systems
• Bounded parametric model checking for elementary net systems
• scientific article; zbMATH DE number 1701759 (Why is no real title available?)
• Bounded model checking with parametric data structures
• Synthesis of bounded integer parameters for parametric timed reachability games
• Bounded model checking for timed automata

Describes a project that uses

Uses Software

• Uppaal
• Moby/DC

This page was built for publication: Bounded Model Checking for Parametric Timed Automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2889614)