Abstract
We study the universality and inclusion problems for register automata over equality data (A, =). We show that the universality L(B) = (Σ × A)^* and inclusion problems L(A) ⊆ L(B) B can be solved with 2EXPTIME complexity when both automata are without guessing and B is unambiguous, improving on the currently bestknown 2EXPSPACE upper bound by Mottet and Quaas. When the number of registers of both automata is fixed, we obtain a lower EXPTIME complexity, also improving the EXPSPACE upper bound from Mottet and Quaas for fixed number of registers. We reduce inclusion to universality, and then we reduce universality to the problem of counting the number of orbits of runs of the automaton. We show that the orbitcounting function satisfies a system of bidimensional linear recursive equations with polynomial coefficients (linrec), which generalises analogous recurrences for the Stirling numbers of the second kind, and then we show that universality reduces to the zeroness problem for linrec sequences. While such a counting approach is classical and has successfully been applied to unambiguous finite automata and grammars over finite alphabets, its application to register automata over infinite alphabets is novel.
We provide two algorithms to decide the zeroness problem for bidimensional linear recursive sequences arising from orbitcounting functions. Both algorithms rely on techniques from linear noncommutative algebra. The first algorithm performs variable elimination and has elementary complexity. The second algorithm is a refined version of the first one and it relies on the computation of the Hermite normal form of matrices over a skew polynomial field. The second algorithm yields an EXPTIME decision procedure for the zeroness problem of linrec sequences, which in turn yields the claimed bounds for the universality and inclusion problems of register automata.
BibTeX  Entry
@InProceedings{barloy_et_al:LIPIcs.STACS.2021.8,
author = {Barloy, Corentin and Clemente, Lorenzo},
title = {{Bidimensional Linear Recursive Sequences and Universality of Unambiguous Register Automata}},
booktitle = {38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021)},
pages = {8:18:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771801},
ISSN = {18688969},
year = {2021},
volume = {187},
editor = {Bl\"{a}ser, Markus and Monmege, Benjamin},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/13653},
URN = {urn:nbn:de:0030drops136533},
doi = {10.4230/LIPIcs.STACS.2021.8},
annote = {Keywords: unambiguous register automata, universality and inclusion problems, multidimensional linear recurrence sequences}
}
Keywords: 

unambiguous register automata, universality and inclusion problems, multidimensional linear recurrence sequences 
Collection: 

38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021) 
Issue Date: 

2021 
Date of publication: 

10.03.2021 