Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL

DOI10.1007/978-3-642-03359-9_29zbMath1252.68196MaRDI QIDQ3183543

Alexander Schimpf, Jan-Georg Smaus, Stephan Merz

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

Mathematics Subject Classification ID

03D05: Automata and formal grammars in connection with logical questions

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

03B44: Temporal logic

Related Items

Formally verified algorithms for upper-bounding state space diameters, Automatic refinement to efficient data structures: a comparison of two approaches

Uses Software

• Isabelle
• Isabelle/HOL
• LTL2BA
• lbtt

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