Quantitative finite-state systems, such as quantitative automata and graph games, are typically time-symmetric. We investigate the consequences of introducing geometric decay into these systems, through the lenses of discounted-sum automata (NDAs) and Robin Hood bidding games.
NDAs are nondeterministic finite automata equipped with transition weights, where the value of a run is the discounted sum of its weights, and the value of a word is the minimum value over all its accepting runs. The determinization problem asks whether, given an NDA, there exists a deterministic discounted-sum automaton (DDA) that assigns the exact same value to every word. We prove that the determinization problem for NDAs with integral discounting factors is decidable. Specifically, we provide an EXPSPACE algorithm to decide determinizability alongside an explicit construction for the equivalent DDA, and we establish a PSPACE-hardness lower bound for the problem.
As for graph games, we focus on Bidding Games, where players are allocated monetary budgets and bid in auctions to determine movement along the graph. We enrich this model with a wealth-redistribution phase before each turn, which discounts the difference between the players’ budgets. For reachability objectives, we prove the existence of a threshold function - the exact initial budget required for the reachability player to guarantee a win.
We place the associated computational problem in NP. We also reveal that, unlike traditional models, a Robin Hood game may become undetermined exactly at the threshold. For Büchi objectives, we provide a computable candidate for a threshold.