Verifying the LTL to Büchi automata translation via very weak alternating automata

DOI10.1007/978-3-319-94821-8_18OpenAlexW2811364843MaRDI QIDQ1791171

Michael Norrish, Simon Jantsch

Publication date: 4 October 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-94821-8_18

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Temporal logic (03B44) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (2)

Unnamed Item ⋮ Verified Decision Procedures for Modal Logics.

Uses Software

• Isabelle/HOL
• PROMELA
• CakeML

This page was built for publication: Verifying the LTL to Büchi automata translation via very weak alternating automata