Determinization of Integral Discounted-Sum Automata is Decidable
For researchers in automata theory and formal verification, this provides a decidability result for a key problem in discounted-sum automata, though the restriction to integer discount factors limits its generality.
The paper proves that determinization of nondeterministic discounted-sum automata (NDAs) is decidable when the discount factor is a natural number, resolving a previously open problem. This extends prior results that required completeness assumptions.
Nondeterministic Discounted-Sum Automata (NDAs) are nondeterministic finite automata equipped with a discounting factor $λ>1$, and whose transitions are labelled by weights. The value of a run of an NDA is the discounted sum of the edge weights, where the $i$-th weight is divided by $λ^{i}$. NDAs are a useful tool for modelling systems where the values of future events are less influential than immediate ones. While several problems are undecidable or open for NDA, their deterministic fragment (DDA) admits more tractable algorithms. Therefore, determinization of NDAs (i.e., deciding if an NDA has a functionally-equivalent DDA) is desirable. Previous works establish that when $λ\in \mathbb{N}$, then every complete NDA, namely an NDA whose states are all accepting and its transition function is complete, is determinizable. This, however, no longer holds when the completeness assumption is dropped. We show that the problem of whether an NDA has an equivalent DDA is decidable when $λ\in \mathbb{N}$.