History-Determinism vs Fair Simulation
For researchers in automata theory and verification, this work simplifies the decision problem for guidability by linking it to the better-understood history-determinism, with broad applicability across multiple automata classes.
The paper establishes that for many common automata classes, including ω-regular automata and infinite-state automata with safety/reachability conditions, the notions of history-determinism and guidability coincide, enabling reduction of guidability to history-determinism. It provides sufficient criteria for this coincidence and identifies cases where they diverge, such as timed automata with a fixed number of clocks.
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.