eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-02
129:1
129:16
10.4230/LIPIcs.ICALP.2021.129
article
New Techniques for Universality in Unambiguous Register Automata
Czerwiński, Wojciech
1
https://orcid.org/0000-0002-6169-868X
Mottet, Antoine
2
https://orcid.org/0000-0002-3517-1745
Quaas, Karin
3
University of Warsaw, Poland
Department of Algebra, Faculty of Mathematics and Physics, Charles University, Prague, Czech Republic
University of Leipzig, Germany
Register automata are finite automata equipped with a finite set of registers ranging over the domain of some relational structure like (ℕ; =) or (ℚ; <). Register automata process words over the domain, and along a run of the automaton, the registers can store data from the input word for later comparisons. It is long known that the universality problem, i.e., the problem to decide whether a given register automaton accepts all words over the domain, is undecidable. Recently, we proved the problem to be decidable in 2-ExpSpace if the register automaton under study is over (ℕ; =) and unambiguous, i.e., every input word has at most one accepting run; this result was shortly after improved to 2-ExpTime by Barloy and Clemente. In this paper, we go one step further and prove that the problem is in ExpSpace, and in PSpace if the number of registers is fixed. Our proof is based on new techniques that additionally allow us to show that the problem is in PSpace for single-register automata over (ℚ; <). As a third technical contribution we prove that the problem is decidable (in ExpSpace) for a more expressive model of unambiguous register automata, where the registers can take values nondeterministically, if defined over (ℕ; =) and only one register is used.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol198-icalp2021/LIPIcs.ICALP.2021.129/LIPIcs.ICALP.2021.129.pdf
Register Automata
Data Languages
Unambiguity
Unambiguous
Universality
Containment
Language Inclusion
Equivalence