conference paper published yes Udi Boker author 31E297B6-F248-11E8-B48F-1D18A9856A87 Thomas A Henzinger author 40876CD8-F248-11E8-B48F-1D18A9856A870000-0002-2985-7724 Karoliina Lehtinen author Aditya Prakash author ToHe department CONCUR: Conference on Concurrency Theory Vigilant Algorithmic Monitoring of Software project 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 C of automata if it can fairly simulate every automaton in C, 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 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. https://research-explorer.ista.ac.at/download/18067/18080/2024_LIPICS_Boker.pdf application/pdfno https://creativecommons.org/licenses/by/4.0/ Schloss Dagstuhl - Leibniz-Zentrum für Informatik2024Calgary, Canada eng 1868-8969 9783959773393 2407.08620 00155684740001210.4230/LIPIcs.CONCUR.2024.12 311 U. Boker, T. A. Henzinger, K. Lehtinen, and A. Prakash, “History-determinism vs fair simulation,” in <i>35th International Conference on Concurrency Theory</i>, Calgary, Canada, 2024, vol. 311. Boker, Udi, Thomas A Henzinger, Karoliina Lehtinen, and Aditya Prakash. “History-Determinism vs Fair Simulation.” In <i>35th International Conference on Concurrency Theory</i>, Vol. 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2024.12">https://doi.org/10.4230/LIPIcs.CONCUR.2024.12</a>. Boker U, Henzinger TA, Lehtinen K, Prakash A. 2024. History-determinism vs fair simulation. 35th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 311, 12. Boker, Udi, et al. “History-Determinism vs Fair Simulation.” <i>35th International Conference on Concurrency Theory</i>, vol. 311, 12, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2024.12">10.4230/LIPIcs.CONCUR.2024.12</a>. U. Boker, T.A. Henzinger, K. Lehtinen, A. Prakash, in:, 35th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. Boker U, Henzinger TA, Lehtinen K, Prakash A. History-determinism vs fair simulation. In: <i>35th International Conference on Concurrency Theory</i>. Vol 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2024.12">10.4230/LIPIcs.CONCUR.2024.12</a> Boker, U., Henzinger, T. A., Lehtinen, K., &#38; Prakash, A. (2024). History-determinism vs fair simulation. In <i>35th International Conference on Concurrency Theory</i> (Vol. 311). Calgary, Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2024.12">https://doi.org/10.4230/LIPIcs.CONCUR.2024.12</a> 180672024-09-15T22:01:40Z2025-12-02T13:44:54Z