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

DOI10.1007/S10703-021-00379-ZMaRDI QIDQ2147688zbMATH OpenOpenAlexFDO

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

Publication date 20 June 2022

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

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

verificationlinear temporal logicalternating automata\(\omega\)-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)

Abstract: This paper proposes a new algorithm for the generation of unambiguous B"uchi automata (UBA) from LTL formulas. Unlike existing tableau-based LTL-to-UBA translations, our algorithm deals with very weak alternating automata (VWAA) as an intermediate representation. It relies on a new notion of unambiguity for VWAA and a disambiguation procedure for VWAA. We introduce optimizations on the VWAA level and new LTL simplifications targeted at generating small UBA. We report on an implementation of the construction in our tool duggi and discuss experimental results that compare the automata sizes and computation times of duggi with the tableau-based LTL-to-UBA translation of the SPOT tool set. Our experiments also cover the analysis of Markov chains under LTL specifications, which is an important application of UBA.

Recommendations

• scientific article; zbMATH DE number 1796123
• Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata
• LTL to Büchi automata translation: fast and more deterministic
• Concepts of Automata Construction from LTL
• A Unified Translation of Linear Temporal Logic to ω-Automata

Cites work

• scientific article; zbMATH DE number 1670781 (Why is no real title available?)
• scientific article; zbMATH DE number 6527944 (Why is no real title available?)
• scientific article; zbMATH DE number 1479635 (Why is no real title available?)
• scientific article; zbMATH DE number 1487477 (Why is no real title available?)
• scientific article; zbMATH DE number 1759492 (Why is no real title available?)
• scientific article; zbMATH DE number 1759609 (Why is no real title available?)
• scientific article; zbMATH DE number 1796123 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Alternating automata on infinite trees
• An optimal automata approach to LTL model checking of probabilistic systems
• Automata, logics, and infinite games. A guide to current research
• Boolean functions as models for quantified Boolean formulas
• Efficient inclusion testing for simple classes of unambiguous \(\omega \)-automata
• Efficient minimization of deterministic weak -automata
• Equivalence and inclusion problem for strongly unambiguous Büchi automata
• From linear time to branching time
• LTL model checking of interval Markov chains
• LTL to Büchi automata translation: fast and more deterministic
• LTL to deterministic Emerson-Lei automata
• Lazy probabilistic model checking without determinisation
• Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14--19, 2013. Proceedings
• Manipulating LTL Formulas Using Spot 1.0
• Markov chains and unambiguous Büchi automata
• ON THE DISAMBIGUATION OF FINITE AUTOMATA AND FUNCTIONAL TRANSDUCERS
• On the Equivalence and Containment Problems for Unambiguous Regular Expressions, Regular Grammars and Finite Automata
• Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra
• The Complexity of Generalized Satisfiability for Linear Temporal Logic
• The complexity of propositional linear temporal logics
• The logic of ``initially and ``next: complete axiomatization and complexity
• Unambiguity in automata theory
• Unambiguous Büchi automata.

Cited in

(5)

• Singly exponential translation of alternating weak Büchi automata to unambiguous Büchi automata
• Markov chains and unambiguous Büchi automata
• Concepts of Automata Construction from LTL
• A fragment of linear temporal logic for universal very weak automata
• From LTL to unambiguous Büchi automata via disambiguation of alternating automata

Describes a project that uses

Uses Software

• Delag
• LTL2BA
• SPOT

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2147688)