From LTL to unambiguous Büchi automata via disambiguation of alternating automata
Publikation: Beitrag in Fachzeitschrift › Forschungsartikel › Beigetragen › Begutachtung
Beitragende
Abstract
Due to the high complexity of translating linear temporal logic (LTL) to deterministic automata, several forms of “restricted” nondeterminism have been considered with the aim of maintaining some of the benefits of deterministic automata, while at the same time allowing more efficient translations from LTL. One of them is the notion of unambiguity. This paper proposes a new algorithm for the generation of unambiguous Büchi automata (UBA) from LTL formulas. Unlike other approaches it is based on a known translation from very weak alternating automata (VWAA) to NBA. A notion of unambiguity for alternating automata is introduced and it is shown that the VWAA-to-NBA translation preserves unambiguity. Checking unambiguity of VWAA is determined to be PSPACE-complete, both for the explicit and symbolic encodings of alternating automata. The core of the LTL-to-UBA translation is an iterative disambiguation procedure for VWAA. Several heuristics are introduced for different stages of the procedure. We report on an implementation of our approach in the tool Duggi and compare it to an existing LTL-to-UBA implementation in the SPOT tool set. Our experiments cover model checking of Markov chains, which is an important application of UBA.
Details
Originalsprache | Englisch |
---|---|
Seiten (von - bis) | 42–82 |
Seitenumfang | 41 |
Fachzeitschrift | Formal Methods in System Design |
Jahrgang | 58 |
Ausgabenummer | 1-2 |
Publikationsstatus | Veröffentlicht - Okt. 2021 |
Peer-Review-Status | Ja |
Externe IDs
Scopus | 85121381299 |
---|---|
ORCID | /0000-0002-5321-9343/work/142236685 |
Schlagworte
DFG-Fachsystematik nach Fachkollegium
Fächergruppen, Lehr- und Forschungsbereiche, Fachgebiete nach Destatis
ASJC Scopus Sachgebiete
Schlagwörter
- Unambiguous Büchi Automata, alternating automata, linear temporal logic, omega-automata, verification, Alternating automata, Linear temporal logic, Unambiguous Büchi automata, Verification, ω-Automata