On Expressiveness and Complexity in Real-Time Model Checking

DOI10.1007/978-3-540-70583-3_11MaRDI QIDQ3519496zbMATH OpenOpenAlexFDO

Authors Patricia Bouyer, Nicolas Markey, Joël Ouaknine, James Worrell

Publication date 19 August 2008

Published in Automata, Languages and Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-70583-3_11

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Recommendations

• Model-checking in dense real-time
• Correctness of efficient real-time model checking
• Model-checking for real-time systems
• Model Checking Real-Time Systems
• Conformance checking of real-time models. Symbolic execution vs. bounded model checking
• Comparing model checking and logical reasoning for real-time systems
• Compositional Abstraction in Real-Time Model Checking
• Exact acceleration of real-time model checking
• A space-efficient on-the-fly algorithm for real-time model checking

Cited in

(19)

• Model-checking timed temporal logics
• Metric temporal logic revisited
• Spotlight abstraction in model checking real-time task schedulability
• A survey on temporal logics for specifying and verifying real-time systems
• Parameterized model checking of weighted networks
• Bounded model checking for knowledge and real time
• Parametric real-time model checking using splitting trees
• On expressive powers of timed logics: comparing boundedness, non-punctuality, and deterministic freezing
• Realizability of real-time logics
• A logical characterization of timed regular languages
• Real-Time Model Checking on Secondary Storage
• Revisiting MITL to fix decision procedures
• Time-Bounded Verification
• Model checking flat Freeze LTL on one-counter automata
• Model Checking Real-Time Systems
• The complexity of flat freeze LTL
• The complexity of flat freeze LTL
• Some Recent Results in Metric Temporal Logic
• Efficient CTMC Model Checking of Linear Real-Time Objectives

This page was built for publication: On Expressiveness and Complexity in Real-Time Model Checking

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