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

DOI10.1007/978-3-642-03359-9_29zbMath1252.68196OpenAlexW2127726675MaRDI 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

Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items (6)

Formally verified algorithms for upper-bounding state space diameters ⋮ Automatic refinement to efficient data structures: a comparison of two approaches ⋮ Unnamed Item ⋮ A Verified Compositional Algorithm for AI Planning ⋮ Verified Decision Procedures for Modal Logics. ⋮ UNITY and Büchi automata

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

This page was built for publication: Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL