A Brief History of History-Determinism (Invited Talk)

Author Karoliina Lehtinen



PDF
Thumbnail PDF

File

LIPIcs.STACS.2023.1.pdf
  • Filesize: 397 kB
  • 2 pages

Document Identifiers

Author Details

Karoliina Lehtinen
  • CNRS, Aix-Marseille University, LIS, Marseille, France

Cite AsGet BibTex

Karoliina Lehtinen. A Brief History of History-Determinism (Invited Talk). In 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 254, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.STACS.2023.1

Abstract

Most nondeterministic automata models are more expressive, or at least more succinct, than their deterministic counterparts; however, this comes at a cost, as deterministic automata tend to have better algorithmic properties. History-deterministic automata are an intermediate model that allows a restricted form of nondeterminism: all nondeterministic choices must be resolvable on-the-fly, with only the knowledge of the word prefix read so far - as opposed to general nondeterminism, which allows for guessing the future of the word. History-deterministic automata combine some of the algorithmic benefits of determinism with some of the increased power of nondeterminism, thus enjoying (some of) the best of both worlds. History-determinism, as it is understood today, has its roots in several independently invented notions: Kupferman, Safra and Vardi’s automata recognising tree languages derived from word languages [Kupferman et al., 2006] (a notion that has been later referred to as automata that are good-for-trees [Udi Boker et al., 2013]), Henzinger and Piterman’s good-for-games automata [Thomas Henzinger and Nir Piterman, 2006], and Colcombet’s history-deterministic automata, introduced in his work on regular cost-automata [Colcombet, 2009]. In the ω-regular setting, where they were initially most studied, the notions of good-for-trees, good-for-games and history-determinism are equivalent, despite differences in their definitions. The key algorithmic appeal of these automata is that like deterministic automata, they have good compositional properties. This makes them particularly useful for applications such as reactive synthesis, where composition of games and automata is at the heart of effective solutions. Since then, history-determinism has received its fair share of attention, not least because of its relevance to synthesis. Indeed it turns out to be a natural and useful form of nondeterminism more broadly, and can be generalised to all sorts of different automata models: alternating automata [Udi Boker and Karoliina Lehtinen, 2019], pushdown automata [Enzo Erlich et al., 2022; Enzo Erlich et al., 2022], timed automata [Thomas A. Henzinger et al., 2022; Sougata Bose et al., 2022], Parikh automata [Enzo Erlich et al., 2022], and quantiative automata [Udi Boker and Karoliina Lehtinen, 2021], to name a few. In each of these models, history-determinism offers some trade-offs between the power of nondeterminism and the algorithmic properties of determinism. In particular, depending on the model, they can be either more expressive or more succinct than their deterministic counterparts, while retaining better algorithmic properties - in particular with respect to deciding universality, language inclusion and games - than fully nondeterministic automata. The drive to extend history-determinism to more powerful automata models has also lead to a better understanding of the properties of these automata, of how they compare to related notions (such as good-for-games automata and determinisability by pruning), and of the various games and tools used to study them. This talk aims to give a broad introduction to the notion of history determinism as well as an overview of some of the recent developements on the topic. It will also highlight some of the many problems that remain open. It is loosely based on a recent survey, written jointly with Udi Boker, which gives an informal presentation of what are, in our view, the key aspects of history-determinism [Udi Boker and Karoliina Lehtinen, 2023].

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • History-determinism
  • nondeterminism
  • automata
  • good-for-games

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Udi Boker, Denis Kuperberg, Orna Kupferman, and Michał Skrzypczak. Nondeterminism in the presence of a diverse or unknown future. In Proceedings of ICALP, pages 89-100, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_11.
  2. Udi Boker and Karoliina Lehtinen. Good for games automata: From nondeterminism to alternation. In Proceedings of CONCUR, pages 19:1-19:16, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.19.
  3. Udi Boker and Karoliina Lehtinen. History determinism vs. good for gameness in quantitative automata. In Proc. of FSTTCS, pages 35:1-35:20, 2021. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2021.38.
  4. Udi Boker and Karoliina Lehtinen. When a little nondeterminism goes a long way: An introduction to history-determinism. ACM SIGLOG News, 10(1):24–51, Feb 2023. URL: https://doi.org/10.1145/3584676.3584682.
  5. Sougata Bose, Thomas A. Henzinger, Karoliina Lehtinen, Sven Schewe, and Patrick Totzke. History-deterministic timed automata are not determinizable. In Proceedings of RP, pages 67-76, 2022. URL: https://doi.org/10.1007/978-3-031-19135-0_5.
  6. Thomas Colcombet. The theory of stabilisation monoids and regular cost functions. In Proceedings of ICALP, pages 139-150, 2009. URL: https://doi.org/10.1007/978-3-642-02930-1_12.
  7. Enzo Erlich, Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. History-deterministic parikh automata. CoRR, 2022. URL: https://doi.org/10.48550/arXiv.2209.07745.
  8. Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. A bit of nondeterminism makes pushdown automata expressive and succinct, 2022. URL: https://doi.org/10.48550/arXiv.2105.02611.
  9. Thomas Henzinger and Nir Piterman. Solving games without determinization. In Proceedings of CSL, pages 395-410, 2006. URL: https://doi.org/10.1007/11874683_26.
  10. Thomas A. Henzinger, Karoliina Lehtinen, and Patrick Totzke. History-deterministic timed automata. In Proceedings of CONCUR, pages 14:1-14:21, 2022. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2022.14.
  11. Orna Kupferman, Shmuel Safra, and Moshe Y Vardi. Relating word and tree automata. Ann. Pure Appl. Logic, 138(1-3):126-146, 2006. Conference version in 1996. URL: https://doi.org/10.1016/j.apal.2005.06.009.
  12. Karoliina Lehtinen and Martin Zimmermann. Good-for-games ω-pushdown automata. Log. Methods Comput. Sci., 18(1), 2022. Conference version at LICS 2020. URL: https://doi.org/10.46298/lmcs-18(1:3)2022.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail