From LTL to unambiguous Büchi automata via disambiguation of alternating automata

DOI10.1007/s10703-021-00379-zzbMath1505.68022arXiv1907.02887OpenAlexW2953711673MaRDI QIDQ2147688

David Müller, Joachim Klein, Simon Jantsch, Christel Baier

Publication date: 20 June 2022

Published in: Formal Methods in System Design (Search for Journal in Brave)

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

zbMATH Keywords

verification\(\omega\)-automatalinear temporal logicalternating automataunambiguous Büchi automata

Mathematics Subject Classification ID

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

Uses Software

• SPOT
• LTL2BA
• Delag

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The logic of ``initially and ``next: complete axiomatization and complexity
• Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14--19, 2013. Proceedings
• Efficient inclusion testing for simple classes of unambiguous \(\omega \)-automata
• Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra
• Alternating automata on infinite trees
• Unambiguous Büchi automata.
• Efficient minimization of deterministic weak \(\omega\)-automata
• Automata, logics, and infinite games. A guide to current research
• Boolean functions as models for quantified Boolean formulas
• LTL to Büchi Automata Translation: Fast and More Deterministic
• Equivalence and Inclusion Problem for Strongly Unambiguous Büchi Automata
• The Complexity of Generalized Satisfiability for Linear Temporal Logic
• On the Equivalence and Containment Problems for Unambiguous Regular Expressions, Regular Grammars and Finite Automata
• The complexity of propositional linear temporal logics
• Markov Chains and Unambiguous Büchi Automata
• Manipulating LTL Formulas Using Spot 1.0
• From linear time to branching time
• LTL Model Checking of Interval Markov Chains
• Lazy probabilistic model checking without determinisation
• ON THE DISAMBIGUATION OF FINITE AUTOMATA AND FUNCTIONAL TRANSDUCERS
• Unambiguity in Automata Theory

This page was built for publication: From LTL to unambiguous Büchi automata via disambiguation of alternating automata