From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata

DOI10.1007/978-3-662-54577-5_25zbMath1452.68105arXiv1701.06103OpenAlexW3122348209MaRDI QIDQ3303906

Salomon Sickert, Jan Křetínský, Javier Esparza, Jean-François Raskin

Publication date: 5 August 2020

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1701.06103

zbMATH Keywords

regular languagelinear temporal logicsynthesis problemsmall indexacceptance condition

Mathematics Subject Classification ID

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

Related Items (8)

Runtime enforcement of hyperproperties ⋮ On the power of finite ambiguity in Büchi complementation ⋮ A survey on satisfiability checking for the \(\mu \)-calculus through tree automata ⋮ Unnamed Item ⋮ New Optimizations and Heuristics for Determinization of Büchi Automata ⋮ Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis ⋮ Generic Emptiness Check for Fun and Profit ⋮ Practical synthesis of reactive systems from LTL specifications via parity games

Uses Software

• SPOT

Cites Work

• Unnamed Item
• Unnamed Item
• Profile trees for Büchi word automata, with application to determinization
• Limit deterministic and probabilistic automata for \(\mathrm{LTL}\backslash GU\)
• Complementing semi-deterministic Büchi automata
• Comparison of LTL to Deterministic Rabin Automata Translators
• An Improved Construction of Deterministic Omega-automaton Using Derivatives
• Bounded Synthesis for Petri Games
• Weak alternating automata are not that weak
• The complexity of probabilistic verification
• Limit-Deterministic Büchi Automata for Linear Temporal Logic
• From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
• Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
• Correct Hardware Design and Verification Methods

This page was built for publication: From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata