2026-07-25T01:58:13Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:19031 2024-03-06T11:03:19Z ddc:004 open_access

Singly Exponential Translation of Alternating Weak Büchi Automata to Unambiguous Büchi Automata Li, Yong Schewe, Sven Vardi, Moshe Y. Büchi automata unambiguous automata alternation weak disambiguation We introduce a method for translating an alternating weak Büchi automaton (AWA), which corresponds to a Linear Dynamic Logic (LDL) formula, to an unambiguous Büchi automaton (UBA). Our translations generalise constructions for Linear Temporal Logic (LTL), a less expressive specification language than LDL. In classical constructions, LTL formulas are first translated to alternating very weak automata (AVAs) - automata that have only singleton strongly connected components (SCCs); the AVAs are then handled by efficient disambiguation procedures. However, general AWAs can have larger SCCs, which complicates disambiguation. Currently, the only available disambiguation procedure has to go through an intermediate construction of nondeterministic Büchi automata (NBAs), which would incur an exponential blow-up of its own. We introduce a translation from general AWAs to UBAs with a singly exponential blow-up, which also immediately provides a singly exponential translation from LDL to UBAs. Interestingly, the complexity of our translation is smaller than the best known disambiguation algorithm for NBAs (broadly (0.53n)ⁿ vs. (0.76n)ⁿ), while the input of our construction can be exponentially more succinct. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Yong Li and Sven Schewe and Moshe Y. Vardi 2023 Is Part Of LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2023.37 urn:nbn:de:0030-drops-190313 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.37 eng https://creativecommons.org/licenses/by/4.0/legalcode