A space-efficient on-the-fly algorithm for real-time model checking

DOI10.1007/3-540-61604-7_73MaRDI QIDQ6162102zbMATH OpenOpenAlexFDO

Authors Thomas A. Henzinger, Orna Kupferman, Moshe Y. Vardi

Publication date 28 June 2023

Published in CONCUR '96: Concurrency Theory (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-61604-7_73

Mathematics Subject Classification ID

Temporal logic (03B44) 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

• scientific article; zbMATH DE number 1487477
• Model-checking for real-time systems
• Symbolic model checking for real-time systems
• On-the-fly probabilistic model checking
• Model-checking in dense real-time

Cites work

• A really temporal logic
• A theory of timed automata
• Alternating automata on infinite trees
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 3757688 (Why is no real title available?)
• scientific article; zbMATH DE number 177509 (Why is no real title available?)
• scientific article; zbMATH DE number 3999901 (Why is no real title available?)
• Model-checking in dense real-time
• Real-time logics: Complexity and expressiveness
• Reasoning about infinite computations
• Symbolic model checking for real-time systems
• The benefits of relaxing punctuality
• The complexity of propositional linear temporal logics

Cited in

(10)

• Compact data structures and state-space reduction for model-checking real-time systems
• Correctness of efficient real-time model checking
• scientific article; zbMATH DE number 1696514 (Why is no real title available?)
• Automata theory and model checking
• MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs
• On Expressiveness and Complexity in Real-Time Model Checking
• scientific article; zbMATH DE number 1487477 (Why is no real title available?)
• On-the-fly probabilistic model checking
• Real-Time Model Checking on Secondary Storage
• On-the-fly TCTL model checking for time Petri nets

This page was built for publication: A space-efficient on-the-fly algorithm for real-time model checking

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