Token Games and History-Deterministic Quantitative-Automata

TL;DR

The paper advances history-determinism (HD) from the Boolean to the quantitative automata setting by extending token games. It proves that 1-token games $G_1$ characterise HDness for all quantitative (and Boolean) automata on finite words and for several infinite-word classes (Safety, Reachability, Inf, DSum), while 2-token games $G_2$ capture HDness for LimSup, LimInf, and Sup on infinite words, via a decomposition into Büchi/coBüchi components and parity/coBüchi reductions. These characterisations yield concrete, often efficient decision procedures: PTIME for Safety/Reachability/Inf, NP$\cap$coNP for DSum, quasipolynomial (or polynomial when the weight count is small) for LimSup, and exponential in the number of weights for LimInf, with polynomial memory bounds in favorable cases. By tying HDness to best-value synthesis, the work provides direct methods to decide synthesis realizability and construct witness strategies, and it outlines open questions for broader classes such as parity/limit-average automata.

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 HDness problem) is generally a difficult task, which can involve an exponential procedure, or even be undecidable, as is the case for example with pushdown automata. Token games provide a PTime solution to the HDness problem of Büchi and coBüchi automata, and it is conjectured that 2-token games characterise HDness for all $ω$-regular automata. We extend token games to the quantitative setting and analyse their potential to help deciding HDness of quantitative automata. In particular, we show that 1-token games characterise HDness for all quantitative (and Boolean) automata on finite words, as well as discounted-sum (DSum), Inf and Reachability automata on infinite words, and that 2-token games characterise HDness of LimInf and LimSup automata, as well as Sup automata on infinite words. Using these characterisations, we provide solutions to the HDness problem of Safety, Reachability, Inf and Sup automata on finite and infinite words in PTime, of DSum automata on finite and infinite words in NP$\cap$co-NP, of LimSup automata in quasipolynomial time, and of LimInf automata in exponential time, where the latter two are only polynomial for automata with a logarithmic number of weights.

Figures (6)

• Figure 1: An automaton ${\mathcal{A}}$, demonstrating that the ${\mathsf{Reachability}}\xspace$ value function on infinite words is not present-focused: the strategy of Eve that remains forever in $s_0$ is cautious, but does not win the letter game on ${\mathcal{A}}$. The ${\mathsf{Reachability}}\xspace$ automaton ${\mathcal{B}}$ demonstrates another difference between reachability on finite and infinite words: It is HD on infinite words, but not HD on finite words.
• Figure 2: A ${\mathsf{Sup}}\xspace$ automaton ${\mathcal{A}}$, demonstrating that $G_1$ does not characterise history-determinism for ${\mathsf{Sup}}\xspace$ automata on infinite words: ${\mathcal{A}}$ is not HD as Adam can play $a$ when Eve's run is in $s_0$ and $b$ when Eve's run is in $s_1$. If Eve stays in $s_0$, then the word has value 1 and Eve's run has value 0; if Eve goes to $s_1$, then the word has value 3 but Eve's run has value 2. Eve wins $G_1$ by moving to $s_1$ once Adam's token is in $s_1$. If Adam stays in $s_0$, they have the same run; if Adam moves and plays $b$ before Eve moves, she gets value 3 and wins; if he doesn't, then Eve gets the same value as Adam.
• Figure 3: An example of a ${\mathsf{DSum}}\xspace$ automaton ${\mathcal{A}}$ and the corresponding ${\mathsf{DSum}}\xspace$ game $G$ with multiple discount factors, as per the proof of \ref{['cl:DSum-NPcoNP']}, such that Eve wins $G1({\mathcal{A}})$ if and only if she wins $G$ with respect to the non-strict $0$-threshold. Rectangular positions in $G$ are of Adam and ellipses of Eve.
• Figure 4: The flow of arguments for showing that $G_2({\mathcal{A}}) \implies \textsf{HD}\xspace({\mathcal{A}})$ for a ${\mathsf{LimInf}}\xspace$ or ${\mathsf{LimSup}}\xspace$ automaton ${\mathcal{A}}$.
• Figure 5: A ${\mathsf{LimSup}}\xspace$ automaton ${\mathcal{A}}$ and corresponding Büchi automata ${\mathcal{A}}_2$ and ${\mathcal{A}}_3$, as per \ref{['cl:decomposeG2']}. (Accepting transitions in ${\mathcal{A}}_2$ and ${\mathcal{A}}_3$ are marked with double lines.) Observe that ${\mathcal{A}}$ is not HD and Eve loses the two-token game on ${\mathcal{A}}$, while both ${\mathcal{A}}_2$ and ${\mathcal{A}}_3$ are HD. (In ${\mathcal{A}}$, if Eve goes from $s_0$ to $s_1$, Adam goes from $s_0$ to $s_2$ and continues with an $a$, and if she goes from $s_0$ to $s_2$, Adam goes from $s_0$ to $s_1$ and continues with a $b$. In ${\mathcal{A}}_2$ Eve goes from $s_0$ to $s_1$ and in ${\mathcal{A}}_3$ from $s_0$ to $s_2$.)

Theorems & Definitions (58)

• Proposition 1.1
• Definition 2.1: History-determinism Col09BL21
• Definition 2.2: Cautious strategies BL21
• Definition 2.3: Present-focused value functions BL21
• Proposition 2.4: BL21
• Proposition 2.5: BL21
• Definition 3.1: $k$-token games
• Theorem 4.1
• proof
• Corollary 4.2