On the Comparison of Discounted-Sum Automata with Multiple Discount Factors

TL;DR

This paper investigates the decidability of comparing nondeterministic discounted-sum automata with multiple discount factors, establishing undecidability in general and providing algorithms for specific cases with single discount factors.

Contribution

It proves undecidability for automata with multiple discount factors and offers algorithms for automata with single, possibly different, rational discount factors.

Findings

Decidability holds for automata with single, possibly different, integral discount factors.

Comparison problems are undecidable for automata with multiple discount factors.

Algorithms are provided for checking equivalence and inequalities between nondeterministic and deterministic automata with rational discount factors.

Abstract

We look into the problems of comparing nondeterministic discounted-sum automata on finite and infinite words. That is, the problems of checking for automata $A$ and $B$ whether or not it holds that for all words $w$, $A(w)=B(w), A(w) \leq B(w)$, or $A(w)<B(w)$. These problems are known to be decidable when both automata have the same single integral discount factor, while decidability is open in all other settings: when the single discount factor is a non-integral rational; when each automaton can have multiple discount factors; and even when each has a single integral discount factor, but the two are different. We show that it is undecidable to compare discounted-sum automata with multiple discount factors, even if all are integrals, while it is decidable to compare them if each has a single, possibly different, integral discount factor. To this end, we also provide algorithms to check for given nondeterministic automaton $N$ and deterministic automaton $D$, each with a single, possibly different, rational discount factor, whether or not $N(w) = D(w)$, $N(w) \geq D(w)$, or $N(w) > D(w)$ for all words $w$.