History-Determinism vs Fair Simulation

TL;DR

This paper explores the relationship between history-determinism and guidability in automata, showing they coincide for many classes but not all, impacting model-checking and synthesis applications.

Contribution

It establishes conditions under which history-determinism and guidability coincide, and demonstrates their equivalence for common automata classes, simplifying decision problems.

Findings

Guidability and history-determinism coincide for many automata classes.

Deciding guidability reduces to deciding history-determinism under certain conditions.

They do not always coincide, as shown for timed automata with fixed clocks.

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 $\omega$-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.