New Techniques for Universality in Unambiguous Register Automata
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F21%3A10437944" target="_blank" >RIV/00216208:11320/21:10437944 - isvavai.cz</a>
Výsledek na webu
<a href="https://doi.org/10.4230/LIPIcs.ICALP.2021.129" target="_blank" >https://doi.org/10.4230/LIPIcs.ICALP.2021.129</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.4230/LIPIcs.ICALP.2021.129" target="_blank" >10.4230/LIPIcs.ICALP.2021.129</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
New Techniques for Universality in Unambiguous Register Automata
Popis výsledku v původním jazyce
Register automata are finite automata equipped with a finite set of registers ranging over the domain of some relational structure like (N; =) 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 (N; =) 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 (N; =) and only one register is used. (C) 2021 Wojciech Czerwiński, Antoine Mottet, and Karin Quaas.
Název v anglickém jazyce
New Techniques for Universality in Unambiguous Register Automata
Popis výsledku anglicky
Register automata are finite automata equipped with a finite set of registers ranging over the domain of some relational structure like (N; =) 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 (N; =) 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 (N; =) and only one register is used. (C) 2021 Wojciech Czerwiński, Antoine Mottet, and Karin Quaas.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
—
OECD FORD obor
10101 - Pure mathematics
Návaznosti výsledku
Projekt
—
Návaznosti
R - Projekt Ramcoveho programu EK
Ostatní
Rok uplatnění
2021
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
Leibniz International Proceedings in Informatics, LIPIcs
ISBN
978-3-95977-195-5
ISSN
1868-8969
e-ISSN
—
Počet stran výsledku
16
Strana od-do
1-16
Název nakladatele
Schloss Dagstuhl
Místo vydání
Německo
Místo konání akce
Skotsko
Datum konání akce
12. 7. 2021
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—