Abstract
A nondeterministic automaton is history-deterministic if its nondeterminism can be resolved by only considering the prefix of the word read so far. Due to their good compositional properties, history-deterministic automata are useful in solving games and synthesis problems. Deciding whether a given nondeterministic automaton is history-deterministic (the HDness problem) is generally a difficult task, which might involve an exponential procedure, or even be undecidable, for example for pushdown automata. Token games provide a PTime solution to the HDness problem of Büchi and coBüchi automata, and it is conjectured that 2-token games characterise HDness for all \(\omega \)-regular automata. We extend token games to the quantitative setting and analyze their potential to help deciding HDness for quantitative automata. In particular, we show that 1-token games characterise HDness for all quantitative (and Boolean) automata on finite words, as well as discounted-sum (\({\mathsf {DSum}}\)) automata on infinite words, and that 2-token games characterise HDness of \({\mathsf {LimInf}}\) and \({\mathsf {LimSup}}\) automata. Using these characterisations, we provide solutions to the HDness problem of \({\mathsf {Inf}}\) and \({\mathsf {Sup}}\) automata on finite words in PTime, for \({\mathsf {DSum}}\) automata on finite and infinite words in NP\(\cap \) co-NP, for \({\mathsf {LimSup}}\) automata in quasipolynomial time, and for \({\mathsf {LimInf}}\) automata in exponential time, where the latter two are only polynomial for automata with a logarithmic number of weights.
Chapter PDF
Similar content being viewed by others
References
Benjamin Aminof, Orna Kupferman, and Robby Lampert. Reasoning about online algorithms with weighted automata. ACM Trans. Algorithms, 6(2):28:1–28:36, 2010.
Daniel Andersson. An improved algorithm for discounted payoff games. In Proc. of ESSLLI Student Session, pages 91–98, 2006.
Marc Bagnol and Denis Kuperberg. Büchi good-for-games automata are efficiently recognizable. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018), page 16, 2018.
Udi Boker. Why these automata types? In Proceedings of LPAR, pages 143–163, 2018.
Udi Boker. Quantitative vs. weighted automata. In Proc. of Reachbility Problems, pages 1–16, 2021.
Udi Boker, Denis Kuperberg, Karoliina Lehtinen, and Michał Skrzypczak. On succinctness and recognisability of alternating good-for-games automata. arXiv preprint arXiv:2002.07278, 2020.
Udi Boker and Karoliina Lehtinen. Good for games automata: From nondeterminism to alternation. In Proceedings of CONCUR, volume 140 of LIPIcs, pages 19:1–19:16, 2019.
Udi Boker and Karoliina Lehtinen. History determinism vs. good for gameness in quantitative automata. In Proc. of FSTTCS, pages 35:1–35:20, 2021.
Cristian S Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasipolynomial time. In Proceedings of STOC, pages 252–263, 2017.
Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Quantitative languages. ACM Trans. Comput. Log., 11(4):23:1–23:38, 2010.
Thomas Colcombet. The theory of stabilisation monoids and regular cost functions. In Proceedings of ICALP, pages 139–150, 2009.
Thomas Colcombet and Nathanaël Fijalkow. Universal graphs and good for games automata: New tools for infinite duration games. In Proc. of FOSSACS, volume 11425 of Lecture Notes in Computer Science, pages 1–26. Springer, 2019.
Emmanuel Filiot, Ismaël Jecker, Nathan Lhote, Guillermo A. Pérez, and Jean-François Raskin. On delay and regret determinization of max-plus automata. In LICS, pages 1–12, 2017.
Emmanuel Filiot, Christof Löding, and Sarah Winter. Synthesis from weighted specifications with partial domains over finite words. In Nitin Saxena and Sunil Simon, editors, FSTTCS, volume 182 of LIPIcs, pages 46:1–46:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. A bit of nondeterminism makes pushdown automata expressive and succinct. In Proc. of MFCS, pages 53:1–53:20, 2021.
Thomas Henzinger and Nir Piterman. Solving games without determinization. In Proceedings of CSL, pages 395–410, 2006.
Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin. Minimizing regret in discounted-sum games. In Jean-Marc Talbot and Laurent Regnier, editors, CSL, volume 62 of LIPIcs, pages 30:1–30:17, 2016.
Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin. Reactive synthesis without regret. Acta Informatica, 54(1):3–39, 2017.
Denis Kuperberg and Michał Skrzypczak. On determinisation of good-for-games automata. In Proceedings of ICALP, pages 299–310, 2015.
Karoliina Lehtinen and Martin Zimmermann. Good-for-games \(\omega \)-pushdown automata. In LICS20, pages 689–702, 2020.
Anirban Majumdar and Denis Kuperberg. Computing the width of non-deterministic automata. Logical Methods in Computer Science, 15, 2019.
L. S. Shapley. Stochastic games. In Proc. of Nat. Acad. Sci., volume 39, pages 1095–1100, 1953.
Uri Zwick and Mike Paterson. The complexity of mean payoff games on graphs. Electron. Colloquium Comput. Complex., 2(40), 1995.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Boker, U., Lehtinen, K. (2022). Token Games and History-Deterministic Quantitative Automata. In: Bouyer, P., Schröder, L. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2022. Lecture Notes in Computer Science, vol 13242. Springer, Cham. https://doi.org/10.1007/978-3-030-99253-8_7
Download citation
DOI: https://doi.org/10.1007/978-3-030-99253-8_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99252-1
Online ISBN: 978-3-030-99253-8
eBook Packages: Computer ScienceComputer Science (R0)