Minimizing Cost Register Automata over a Field

TL;DR

This paper addresses the problem of minimizing the number of registers and states in Cost Register Automata over a field, providing algorithms with complexity bounds and extending previous algebraic invariants for weighted automata.

Contribution

It introduces algorithms for minimizing registers and states in CRA over a field using the linear hull invariant, and extends results to affine updates with complexity analysis.

Findings

Algorithms for register and state minimization in CRA are developed.

The register minimization problem is solvable in 2-ExpTime.

The state-register minimization problem is solvable in NExpTime.

Abstract

Weighted automata (WA) are an extension of finite automata that define functions from words to values in a given semiring. An alternative deterministic model, called Cost Register Automata (CRA), was introduced by Alur et al. It enriches deterministic finite automata with a finite number of registers, which store values, updated at each transition using the operations of the semiring. It is known that CRA with register updates defined by linear maps have the same expressiveness as WA. Previous works have studied the register minimization problem: given a function computable by a WA and an integer k, is it possible to realize it using a CRA with at most k registers? In this paper, we solve this problem for CRA over a field with linear register updates, using the notion of linear hull, an algebraic invariant of WA introduced recently by Bell and Smertnig. We then generalise the approach to solve a more challenging problem, that consists in minimizing simultaneously the number of states and that of registers. In addition, we also lift our results to the setting of CRA with affine updates. Last, while the linear hull was recently shown to be computable by Bell and Smertnig, no complexity bounds were given. To fill this gap, we provide two new algorithms to compute invariants of WA. This allows us to show that the register (resp. state-register) minimization problem can be solved in 2-ExpTime (resp. in NExpTime).