Li, Y, Schewe, S 
ORCID: 0000-0002-9093-9518 and Vardi, MY
(2023)
Singly Exponential Translation of Alternating Weak Büchi Automata to Unambiguous Büchi Automata.
.
Abstract
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)n vs. (0.76n)n), while the input of our construction can be exponentially more succinct.
| Item Type: | Conference or Workshop Item (Unspecified) |
|---|---|
| Divisions: | Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science |
| Depositing User: | Symplectic Admin |
| Date Deposited: | 12 Oct 2023 07:46 |
| Last Modified: | 12 Oct 2023 07:47 |
| DOI: | 10.4230/LIPIcs.CONCUR.2023.37 |
| Open Access URL: | https://drops.dagstuhl.de/opus/volltexte/2023/1902... |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3173606 |
Dimensions
Dimensions
