Li, Yong 
ORCID: 0000-0002-7301-9234, Schewe, Sven ORCID: 0000-0002-9093-9518 and Vardi, Moshe Y
(2023)
Singly Exponential Translation of Alternating Weak Büchi Automata to
Unambiguous Büchi Automata.
[Preprint]
|
PDF
CONCUR2023.pdf - Other Download (800kB) | Preview |
Abstract
We introduce a method for translating an alternating weak B\"uchi automaton (AWA), which corresponds to a Linear Dynamic Logic (LDL) formula, to an unambiguous B\"uchi 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 \emph{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\"uchi automata (NBAs), which would incur an exponential blow-up of its own. We introduce a translation from \emph{general} AWAs to UBAs with a \emph{singly} exponential blow-up, which also immediately provides a singly exponential translation from LDL to UBAs. Interestingly, the complexity of our translation is \emph{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: | Preprint |
|---|---|
| Additional Information: | 23 pages |
| Uncontrolled Keywords: | cs.FL, cs.FL, F.4.3 |
| Divisions: | Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science |
| Depositing User: | Symplectic Admin |
| Date Deposited: | 20 Jul 2023 12:46 |
| Last Modified: | 20 Jul 2023 14:56 |
| Related URLs: | |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3171809 |
Share
Share
