Bidimensional linear recursive sequences and universality of unambiguous register automata

We study the universality and inclusion problems for register automata over equality data (A, =). We show that the universality and inclusion problems can be solved with 2-EXPTIME complexity when both automata are without guessing and unambiguous, improving on the currently best-known 2-EXPSPACE upper bound by Mottet and Quaas. 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 orbit-counting function satisfies a system of bidimensional linear recursive equations with polynomial coefficients (linrec), and then we show that universality reduces to the zeroness problem for linrec sequences. We provide two algorithms to decide the zeroness problem for bidimensional linear recursive sequences arising from orbit-counting functions. Both algorithms rely on techniques from linear non-commutative 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.