Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
From MaRDI portal
Publication:3183543
DOI10.1007/978-3-642-03359-9_29zbMath1252.68196MaRDI QIDQ3183543
Stephan Merz, Jan-Georg Smaus, Alexander Schimpf
Publication date: 20 October 2009
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-03359-9_29
03D05: Automata and formal grammars in connection with logical questions
68Q60: Specification and verification (program logics, model checking, etc.)
03B44: Temporal logic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Proof methods for modal and intuitionistic logics
- The temporal semantics of concurrent programs
- Reasoning about infinite computations
- Weak alternating automata are not that weak
- Constructing Büchi Automata from Linear Temporal Logic Using Simulation Relations for Alternating Büchi Automata
- Tools and Algorithms for the Construction and Analysis of Systems
- Correct Hardware Design and Verification Methods