Efficient timed model checking for discrete-time systems

DOI10.1016/j.tcs.2005.11.020zbMath1088.68107MaRDI QIDQ2368994

Yanyan Li

Publication date: 28 April 2006

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2005.11.020

zbMATH Keywords

Model checking; Timed automata; Durational Kripke structures; Quantitative temporal logics; Timed transition graphs

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Minimum and maximum delay problems in real-time systems
• Model-checking in dense real-time
• Real-time logics: Complexity and expressiveness
• The complexity of optimization problems
• More complicated questions about maxima and minima, and some closures of NP
• The polynomial-time hierarchy
• A theory of timed automata
• Symbolic model checking for real-time systems
• On the expressivity and complexity of quantitative branching-time temporal logics
• The Verus language: Representing time efficiently with BDDs
• Modalities for model checking: Branching time logic strikes back
• Analysis and verification of real-time systems using quantitative symbolic algorithms
• Is your model checker on time? On the complexity of model checking for timed modal logics
• The Exact Path Length Problem
• The power of the future perfect in program logics
• On the complexity of unique solutions
• The complexity of propositional linear temporal logics
• A really temporal logic
• The benefits of relaxing punctuality
• CONCUR 2004 - Concurrency Theory
• An automata-theoretic approach to branching-time model checking
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Foundations of Software Science and Computational Structures