Document Open Access Logo

History Determinism vs. Good for Gameness in Quantitative Automata

Authors Udi Boker, Karoliina Lehtinen

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2021.38.pdf
  • Filesize: 0.83 MB
  • 20 pages

Document Identifiers

Author Details

Udi Boker
  • Reichman University, Herzliya, Israel
Karoliina Lehtinen
  • CNRS, Marseille-Aix Université, Université de Toulon, LIS, Marseille, France

Acknowledgements

We thank Jan Otop for discussing Borel definability in quantitative automata.

Cite AsGet BibTex

Udi Boker and Karoliina Lehtinen. History Determinism vs. Good for Gameness in Quantitative Automata. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 38:1-38:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.FSTTCS.2021.38

Abstract

Automata models between determinism and nondeterminism/alternations can retain some of the algorithmic properties of deterministic automata while enjoying some of the expressiveness and succinctness of nondeterminism. We study three closely related such models - history determinism, good for gameness and determinisability by pruning - on quantitative automata. While in the Boolean setting, history determinism and good for gameness coincide, we show that this is no longer the case in the quantitative setting: good for gameness is broader than history determinism, and coincides with a relaxed version of it, defined with respect to thresholds. We further identify criteria in which history determinism, which is generally broader than determinisability by pruning, coincides with it, which we then apply to typical quantitative automata types. As a key application of good for games and history deterministic automata is synthesis, we clarify the relationship between the two notions and various quantitative synthesis problems. We show that good-for-games automata are central for "global" (classical) synthesis, while "local" (good-enough) synthesis reduces to deciding whether a nondeterministic automaton is history deterministic.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Good for games
  • history determinism
  • alternation
  • quantitative automata

Metrics

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

References

  1. Shaull Almagor and Orna Kupferman. Good-enough synthesis. In CAV, volume 12225 of Lecture Notes in Computer Science, pages 541-563. Springer, 2020. Google Scholar
  2. Shaull Almagor, Orna Kupferman, Jan Oliver Ringert, and Yaron Velner. Quantitative assume guarantee synthesis. In International Conference on Computer Aided Verification, pages 353-374. Springer, 2017. Google Scholar
  3. Benjamin Aminof, Orna Kupferman, and Robby Lampert. Reasoning about online algorithms with weighted automata. ACM Trans. Algorithms, 6(2):28:1-28:36, 2010. Google Scholar
  4. Roderick Bloem, Krishnendu Chatterjee, Thomas A Henzinger, and Barbara Jobstmann. Better quality in synthesis through quantitative objectives. In International Conference on Computer Aided Verification, pages 140-156. Springer, 2009. Google Scholar
  5. Udi Boker. Quantitative vs. weighted automata. In Proc. of Reachbility Problems, pages 1-16, 2021. Google Scholar
  6. Udi Boker and Guy Hefetz. Discounted-sum automata with multiple discount factors. In Proc. of CSL, volume 183 of LIPIcs, pages 12:1-12:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  7. 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. Google Scholar
  8. 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. Google Scholar
  9. Romain Brenguier, Lorenzo Clemente, Paul Hunter, Guillermo A Pérez, Mickael Randour, Jean-François Raskin, Ocan Sankur, and Mathieu Sassolas. Non-zero sum games for reactive synthesis. In Language and Automata Theory and Applications, pages 3-23. Springer, 2016. Google Scholar
  10. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Alternating weighted automata. In Proceedings of FCT, pages 3-13, 2009. Google Scholar
  11. Thomas Colcombet. The theory of stabilisation monoids and regular cost functions. In Proceedings of ICALP, pages 139-150, 2009. Google Scholar
  12. 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. Google Scholar
  13. Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. A bit of nondeterminism makes pushdown automata expressive and succinct. In MFCS, volume 202 of LIPIcs, pages 53:1-53:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.MFCS.2021.53.
  14. Thomas Henzinger and Nir Piterman. Solving games without determinization. In Proceedings of CSL, pages 395-410, 2006. Google Scholar
  15. Paul Hunter, Arno Pauly, Guillermo A. Pérez, and Jean-François Raskin. Mean-payoff games with partial observation. Theor. Comput. Sci., 735:82-110, 2018. Google Scholar
  16. Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin. Reactive synthesis without regret. In Luca Aceto and David de Frutos-Escrig, editors, CONCUR, volume 42 of LIPIcs, pages 114-127, 2015. Google Scholar
  17. 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. Google Scholar
  18. Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin. Reactive synthesis without regret. Acta Informatica, 54(1):3-39, 2017. Google Scholar
  19. 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. Google Scholar
  20. Donald A. Martin. Borel determinacy. Annals of Mathematics, 102(2), 1975. Google Scholar
  21. Gila Morgenstern. Expressiveness results at the bottom of the ω-regular hierarchy. M.Sc. Thesis, The Hebrew University, 2003. Google Scholar
  22. Wolfgang Thomas. Languages, automata, and logic. In Grzegorz Rozenberg and Arto Salomaa, editors, Handbook of Formal Languages, Volume 3: Beyond Words, pages 389-455. Springer, 1997. Google Scholar
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact