Vector spaces of orbit-finite dimension, with applications to weighted and unambiguous register automata

We develop the theory of vector spaces spanned by orbit-finite sets, with the main technical result being finite upper bounds on the lengths of increasing chains of equivariant subspaces. We then apply this theory to weighted register automata, which are a common generalization of weighted automata and register automata for infinite alphabets. We prove that if the atoms can be compared for equality or order, then the equivalence problem for weighted automata is decidable in exponential space, and in polynomial time for a fixed number of registers. As a consequence, equivalence for unambiguous register automata can be tested with the same complexity. This improves previous results for equivalence of unambiguous register automata: (a) we allow for ordered data, and not just equality; (b) our algorithm is exponentially faster than previous ones; (c) we allow for unambiguous automata with guessing. This is a joint work of Mikołaj Bojańczyk, Bartek Klin and Joshua Moerman.