Token Games and History-Deterministic Quantitative Automata
Udi Boker, Karoliina Lehtinen · Lecture notes in computer science · 2022
Abstract A nondeterministic automaton is history-deterministic if its nondeterminism can be resolved by only considering the prefix of the word read so far. Due to their good compositional properties, history-deterministic automata are useful in solving games and synthesis problems. Deciding whether a given nondeterministic automaton is history-deterministic (the problem) is generally a difficult task, which might involve an exponential procedure, or even be undecidable, for example for pushdown automata.Token gamesprovide aPTimesolution to the problem of Büchi and coBüchi automata, and it is conjectured that 2-token games characterise for all $$\omega $$ ω -regular automata. We extend token games to the quantitative setting and analyze their potential to help deciding for quantitative automata. In particular, we show that 1-token games characterise for all quantitative (and Boolean) automata on finite words, as well as discounted-sum ( $${\mathsf {DSum}}$$ DSum ) automata on infinite words, and that 2-token games characterise of $${\mathsf {LimInf}}$$ LimInf and $${\mathsf {LimSup}}$$ LimSup automata. Using these characterisations, we provide solutions to the problem of $${\mathsf {Inf}}$$ Inf and $${\mathsf {Sup}}$$ Sup automata on finite words inPTime, for $${\mathsf {DSum}}$$ DSum automata on finite and infinite words inNP $$\cap $$ ∩ co-NP, for $${\mathsf {LimSup}}$$ LimSup automata in quasipolynomial time, and for $${\mathsf {LimInf}}$$ LimInf automata in exponential time, where the latter two are only polynomial for automata with a logarithmic number of weights.