Orbit-Finite-Dimensional Vector Spaces and Weighted Register Automata
Mikołaj Bojańczyk, Joanna Fijalkow, Bartek Klin, Joshua Moerman
TL;DR
The paper develops a theory of vector spaces spanned by orbit-finite sets and uses it to decide equivalence for weighted register automata over equality or ordered atoms. It proves a finite length property for equivariant subspaces, enabling an equivalence algorithm with exponential time in the atom-dimension but polynomial time for a fixed number of registers, and reduces language equivalence for unambiguous register automata to the same complexity. It also introduces orbit-finitely spanned automata to enable minimization and provides a robust framework for vector spaces with atoms, including closure properties and duals, while showing a counterexample (vector atoms) where finite length fails. The results collectively improve decidability and complexity for automata over infinite alphabets and have practical implications for unambiguous automata and register-based systems, including cases with atom orderings. The work advances the algebraic and algorithmic toolkit for nominal sets in automata theory, connecting linear-algebraic methods with orbit-finite combinatorics.
Abstract
We develop a theory of vector spaces spanned by orbit-finite sets. Using this theory, we give a decision procedure for equivalence of weighted register automata, which are the common generalization of weighted automata and register automata for infinite alphabets. The algorithm runs in exponential time, and in polynomial time for a fixed number of registers. As a special case, we can decide, with the same complexity, language equivalence for unambiguous register automata, which improves previous results in three ways: (a) we allow for order comparisons on atoms, and not just equality; (b) the complexity is exponentially better; and (c) we allow automata with guessing.