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

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 ) ≤ 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 ) ≥ D ( w ) , or N ( w ) > D ( w ) for all words w .