A discounted-sum automaton (NDA) is a nondeterministic finite automaton withedge weights, valuing a run by the discounted sum of visited edge weights. Moreprecisely, the weight in the i-th position of the run is divided by$\lambda^i$, where the discount factor $\lambda$ is a fixed rational numbergreater than 1. The value of a word is the minimal value of the automaton runson it. Discounted summation is a common and useful measuring scheme, especiallyfor infinite sequences, reflecting the assumption that earlier weights are moreimportant than later weights. Unfortunately, determinization of NDAs, which isoften essential in formal verification, is, in general, not possible. Weprovide positive news, showing that every NDA with an integral discount factoris determinizable. We complete the picture by proving that the integerscharacterize exactly the discount factors that guarantee determinizability: forevery nonintegral rational discount factor $\lambda$, there is anondeterminizable $\lambda$-NDA. We also prove that the class of NDAs withintegral discount factors enjoys closure under the algebraic operations min,max, addition, and subtraction, which is not the case for general NDAs nor fordeterministic NDAs. For general NDAs, we look into approximate determinization,which is always possible as the influence of a word's suffix decays. We showthat the naive approach, of unfolding the automaton computations up to asufficient level, is doubly exponential in the discount factor. We provide analternative construction for approximate determinization, which is singlyexponential in the discount factor, in the precision, and in the number ofstates. We also prove matching lower bounds, showing that the exponentialdependency on each of these three parameters cannot be avoided. All our resultshold equally for automata over finite words and for automata over infinitewords.
展开▼
