Time-Bounded Verification

DOI10.1007/978-3-642-04081-8_33zbMath1254.68151OpenAlexW1523732197MaRDI QIDQ3184695

Joël Ouaknine, Alexander Rabinovich, James Worrell

Publication date: 22 October 2009

Published in: CONCUR 2009 - Concurrency Theory (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-04081-8_33

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Related Items (10)

Timed hyperproperties ⋮ The Expressive Power of Temporal and First-Order Metric Logics ⋮ Time-Bounded Verification of CTMCs against Real-Time Specifications ⋮ Model Checking Real-Time Systems ⋮ Time-Bounded Verification ⋮ Bounded variability of metric temporal logic ⋮ On Reachability for Hybrid Automata over Bounded Time ⋮ The compound interest in relaxing punctuality ⋮ Unnamed Item ⋮ Timed Bounded Verification of Inclusion Based on Timed Bounded Discretized Language

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The complexity of temporal logic over the reals
• Real-time logics: Complexity and expressiveness
• Quantitative temporal logics over the reals: PSpace and below
• Timed automata and recognizability
• Using mappings to prove timing properties
• The monadic theory of order
• Event-clock automata: a determinizable class of timed automata
• A theory of timed automata
• Finite variability interpretation of monadic logic of order
• Future temporal logic needs infinitely many modalities
• Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
• The Theory of Timed I/O Automata, Second Edition
• Time-Bounded Verification
• On Expressiveness and Complexity in Real-Time Model Checking
• The benefits of relaxing punctuality
• Expressiveness of Metric modalities for continuous time
• On the decidability and complexity of Metric Temporal Logic over finite words
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: Time-Bounded Verification