History-Determinism vs Fair Simulation
Udi Boker, Thomas A. Henzinger, Karoliina Lehtinen, Aditya Prakash

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 is guidable with respect to a class of automata if it can fairly simulate every automaton in whose language is contained in that of . 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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
