New Techniques for Universality in Unambiguous Register Automata

TL;DR

This paper advances the understanding of the universality problem for unambiguous register automata, showing it is decidable in ExpSpace and PSpace for fixed registers, with new techniques applicable to various models and structures.

Contribution

It proves the universality problem for unambiguous register automata is in ExpSpace and PSpace for fixed registers, extending previous decidability results with novel methods.

Findings

Universality problem is in ExpSpace for unambiguous register automata over (N;=).

The problem is in PSpace when the number of registers is fixed.

Decidability is established for a more expressive model with nondeterministic register values.

Abstract

Register automata are finite automata equipped with a finite set of registers ranging over the domain of some relational structure like $(\mathbb N;=)$ or $(\mathbb Q;<)$. 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 $(\mathbb 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 $(\mathbb Q;<)$. 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 $(\mathbb N;=)$ and only one register is used.