History-Determinism vs Fair Simulation

TL;DR

History-determinism (HD) enables on-the-fly resolution of nondeterminism, while guidability aligns inclusion with simulation. The paper develops practical criteria—closure under history-determinism, 1-token ghost, and strategy-ghost constructions—to guarantee HD = Guidability for broad automata classes. It proves HD = Guidability for omega-regular automata, safety and reachability timed automata, pushdown, VASS, one-counter and Parikh automata, and visibly pushdown automata, among others, and provides counterexamples in classes with limited resources. As a consequence, guidability becomes decidable with complexity matching history-determinism for many classes, enabling more efficient model-checking workflows. The results point to extensions to finite-word and quantitative automata and suggest broader applicability in verification tasks.

Abstract

An automaton is history-deterministic if its nondeterminism can be resolved on the fly, only using the prefix of the word read so far. This mild form of nondeterminism has attracted particular attention for its applications in synthesis problems. An automaton $A$ is guidable with respect to a class $C$ of automata if it can fairly simulate every automaton in $C$ whose language is contained in that of $A$. In other words, guidable automata are those for which inclusion and simulation coincide, making them particularly interesting for model-checking. We study the connection between these two notions, and specifically the question of when they coincide. For classes of automata on which they do, deciding guidability, an otherwise challenging decision problem, reduces to deciding history-determinism, a problem that is starting to be well-understood for many classes. We provide a selection of sufficient criteria for a class of automata to guarantee the coincidence of the notions, and use them to show that the notions coincide for the most common automata classes, among which are $ω$-regular automata and many infinite-state automata with safety and reachability acceptance conditions, including vector addition systems with states, one-counter nets, pushdown-, Parikh-, and timed-automata. We also demonstrate that history-determinism and guidability do not always coincide, for example, for the classes of timed automata with a fixed number of clocks.

Figures (2)

• Figure 1: A linear automaton which admits no linear automaton that is a $1$-token ghost of it.
• Figure 2: A Büchi automaton that accepts words with a finite number of $a$'s. To simulate any equivalent small enough Büchi automaton ${\mathcal{B}}$, Eve moves to the next accepting state once the other automaton is in a maximally strongly connected component with an accepting state. The size constraint on ${\mathcal{B}}$, and the observation that a such a component can not both have a transition on $a$ and an accepting state guarantees that this strategy wins in the simulation game. However, ${\mathcal{B}}$ is not history-deterministic.

Theorems & Definitions (38)

• Theorem 1
• Definition 2: Simulation game
• Definition 3: $1$-token games over two LTSs (or automata)
• Lemma 3
• Definition 4: 1-token ghost
• Lemma 4
• Definition 5
• Lemma 5
• Lemma 6
• Corollary 7