Experiments with deterministic \(\omega\)-automata for formulas of linear temporal logic

DOI10.1016/j.tcs.2006.07.022zbMath1153.03016OpenAlexW2087107980MaRDI QIDQ860862

Christel Baier, Joachim Klein

Publication date: 9 January 2007

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2006.07.022

zbMATH Keywords

\(\omega\)-automatadeterminizationLTLdeterministic Rabin/Streett automataSafra's algorithm

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Temporal logic (03B44)

Related Items (14)

From LTL to deterministic automata. A safraless compositional approach ⋮ Index appearance record with preorders ⋮ Minimal counterexamples for linear-time probabilistic verification ⋮ On-the-Fly Stuttering in the Construction of Deterministic ω-Automata ⋮ Markov chains and unambiguous automata ⋮ Unnamed Item ⋮ Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis ⋮ Generic Emptiness Check for Fun and Profit ⋮ Index Appearance Record for Transforming Rabin Automata into Parity Automata ⋮ Optimal Translation of LTL to Limit Deterministic Automata ⋮ Functional Encryption for Inner Product with Full Function Privacy ⋮ From LTL to Symbolically Represented Deterministic Automata ⋮ State of Büchi Complementation ⋮ Back to the future: a fresh look at linear temporal logic

Uses Software

• SPIN
• LTL2BA

Cites Work

• Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra
• Efficient minimization of deterministic weak \(\omega\)-automata
• Automata, logics, and infinite games. A guide to current research
• Constructing Büchi Automata from Linear Temporal Logic Using Simulation Relations for Alternating Büchi Automata
• Deciding full branching time logic
• Three Partition Refinement Algorithms
• Correct Hardware Design and Verification Methods
• Implementation and Application of Automata
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Experiments with deterministic \(\omega\)-automata for formulas of linear temporal logic