From LTL to Symbolically Represented Deterministic Automata

DOI10.1007/978-3-540-78163-9_24zbMath1138.68454OpenAlexW1484998667MaRDI QIDQ5452723

Andreas Morgenstern, Klaus Schneider

Publication date: 4 April 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-78163-9_24

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 (5)

Optimal bounds in parametric LTL games ⋮ Unnamed Item ⋮ Optimal Translation of LTL to Limit Deterministic Automata ⋮ The Quest for a Tight Translation of Büchi to co-Büchi Automata ⋮ Functional Encryption for Inner Product with Full Function Privacy

Uses Software

• LTL2BA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Experiments with deterministic \(\omega\)-automata for formulas of linear temporal logic
• Unambiguous Büchi automata.
• Improving Automata Generation for Linear Temporal Logic by Considering the Automaton Hierarchy
• An Efficient Pre-determinization Algorithm
• Solving Games Without Determinization
• Deciding full branching time logic
• From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
• Safraless Compositional Synthesis
• Symbolic Implementation of Alternating Automata
• Correct Hardware Design and Verification Methods
• Implementation and Application of Automata
• Implementation and Application of Automata

This page was built for publication: From LTL to Symbolically Represented Deterministic Automata