[en] A central question in the theory of two-player games over graphs is to understand which objectives are half-positional, that is, which are the objectives for which the protagonist does not need memory to implement winning strategies. Objectives for which both players do not need memory have already been characterized (both in finite and infinite graphs); however, less is known about half-positional objectives. In particular, no characterization of half-positionality is known for the central class of ω-regular objectives.
In this paper, we characterize objectives recognizable by deterministic Büchi automata (a class of ω-regular objectives) that are half-positional, in both finite and infinite graphs. Our characterization consists of three natural conditions linked to the language-theoretic notion of right congruence. Furthermore, this characterization yields a polynomial-time algorithm to decide half-positionality of an objective recognized by a given deterministic Büchi automaton.
Research center :
CREMMI - Modélisation mathématique et informatique
Casares, Antonio; Université de Bordeaux [FR] > LaBRI
Randour, Mickaël ; Université de Mons - UMONS > Faculté des Sciences > Service de Mathématiques effectives
Vandenhove, Pierre ; Université de Mons - UMONS > Faculté des Sciences > Service de Mathématiques effectives ; Université Paris-Saclay, CNRS, ENS Paris-Saclay > LMF
Language :
English
Title :
Half-Positional Objectives Recognized by Deterministic Büchi Automata
Publication date :
06 September 2022
Event name :
International Conference on Concurrency Theory (CONCUR)
Event place :
Warsaw, Poland
Event date :
12-16/09/2022
Event number :
33
Audience :
International
Journal title :
Leibniz International Proceedings in Informatics
ISSN :
1868-8969
Publisher :
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Germany
F.R.S.-FNRS - Fonds de la Recherche Scientifique ANR - Agence Nationale de la Recherche
Funding text :
This work has been partially supported by the ANR Project MAVeriQ (ANR-ANR-20-
CE25-0012). Mickael Randour is an F.R.S.-FNRS Research Associate and a member of the TRAIL
Institute. Pierre Vandenhove is an F.R.S.-FNRS Research Fellow.
Bader Abu Radi and Orna Kupferman. Minimizing GFG transition-based automata. In ICALP, volume 132, pages 100:1–100:16, 2019. doi:10.4230/LIPIcs.ICALP.2019.100.
Bader Abu Radi and Orna Kupferman. Canonicity in GFG and transition-based automata. In GandALF, volume 326, pages 199–215, 2020. doi:10.4204/EPTCS.326.13.
Benjamin Aminof and Sasha Rubin. First-cycle games. Inf. Comput., 254:195–216, 2017. doi:10.1016/j.ic.2016.10.008.
Dana Angluin and Dana Fisman. Regular ω-languages with an informative right congruence. Inf. Comput., 278:104598, 2021. doi:10.1016/j.ic.2020.104598.
Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008.
Alessandro Bianco, Marco Faella, Fabio Mogavero, and Aniello Murano. Exploring the boundary of half-positionality. Ann. Math. Artif. Intell., 62(1-2):55–77, 2011. doi:10.1007/ s10472-011-9250-1.
Roderick Bloem, Krishnendu Chatterjee, and Barbara Jobstmann. Graph games and reactive synthesis. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 921–962. Springer, 2018. doi:10.1007/978-3-319-10575-8_27.
Patricia Bouyer, Antonio Casares, Mickael Randour, and Pierre Vandenhove. Half-positional objectives recognized by deterministic Büchi automata. CoRR, abs/2205.01365, 2022. arXiv: 2205.01365, doi:10.48550/arXiv.2205.01365.
Patricia Bouyer, Ulrich Fahrenberg, Kim G. Larsen, Nicolas Markey, and Jirí Srba. Infinite runs in weighted timed automata with energy constraints. In Franck Cassez and Claude Jard, editors, Formal Modeling and Analysis of Timed Systems, 6th International Conference, FORMATS 2008, Saint Malo, France, September 15-17, 2008. Proceedings, volume 5215 of Lecture Notes in Computer Science, pages 33–47. Springer, 2008. doi:10.1007/978-3-540-85778-5_4.
Patricia Bouyer, Stéphane Le Roux, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove. Games where you can play optimally with arena-independent finite memory. In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs, pages 24:1–24:22. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPIcs.CONCUR.2020.24.
Patricia Bouyer, Nicolas Markey, Mickael Randour, Kim G. Larsen, and Simon Laursen. Average-energy games. Acta Inf., 55(2):91–127, 2018. doi:10.1007/s00236-016-0274-1.
Patricia Bouyer, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove. Arena-independent finite-memory determinacy in stochastic games. In Serge Haddad and Daniele Varacca, editors, 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, volume 203 of LIPIcs, pages 26:1–26:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPIcs.CONCUR.2021.26.
Patricia Bouyer, Mickael Randour, and Pierre Vandenhove. Characterizing omega-regularity through finite-memory determinacy of games on infinite graphs. In Petra Berenbrink and Benjamin Monmege, editors, 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022), volume 219 of Leibniz International Proceedings in Informatics (LIPIcs), pages 16:1–16:16, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.STACS.2022.16.
Véronique Bruyère, Quentin Hautem, and Mickael Randour. Window parity games: an alternative approach toward parity games with time bounds. In Domenico Cantone and Giorgio Delzanno, editors, Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016, Catania, Italy, 14-16 September 2016, volume 226 of EPTCS, pages 135–148, 2016. doi:10.4204/EPTCS.226.10.
Véronique Bruyère, Quentin Hautem, Mickael Randour, and Jean-François Raskin. Energy mean-payoff games. In Wan Fokkink and Rob van Glabbeek, editors, 30th International Conference on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands, volume 140 of LIPIcs, pages 21:1–21:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2019. doi:10.4230/LIPIcs.CONCUR.2019.21.
J. Richard Büchi and Lawrence H. Landweber. Definability in the monadic second-order theory of successor. J. Symb. Log., 34(2):166–170, 1969. doi:10.2307/2271090.
J. Richard Büchi. On a decision method in restricted second order arithmetic. Proc. Internat. Congr. on Logic, Methodology and Philosophy of Science, pages 1–11, 1962.
Antonio Casares. On the minimisation of transition-based Rabin automata and the chromatic memory requirements of Muller conditions. In CSL, volume 216, pages 12:1–12:17, 2022. doi:10.4230/LIPIcs.CSL.2022.12.
Antonio Casares, Thomas Colcombet, and Karoliina Lehtinen. On the size of good-for-games Rabin automata and its link with the memory in Muller games. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022), volume 229, pages 117:1–117:20, 2022. doi:10.4230/LIPIcs.ICALP.2022.117.
Krishnendu Chatterjee and Laurent Doyen. Energy parity games. Theor. Comput. Sci., 458:49–60, 2012. doi:10.1016/j.tcs.2012.07.038.
Krishnendu Chatterjee, Laurent Doyen, Mickael Randour, and Jean-François Raskin. Looking at mean-payoff and total-payoff through windows. Inf. Comput., 242:25–52, 2015. doi: 10.1016/j.ic.2015.03.010.
Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdzinski. Mean-payoff parity games. In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings, pages 178–187. IEEE Computer Society, 2005. doi: 10.1109/LICS.2005.26.
Edmund M. Clarke, I. A. Draghicescu, and Robert P. Kurshan. A unified approch for showing language inclusion and equivalence between various types of omega-automata. Inf. Process. Lett., 46(6):301–308, 1993. doi:10.1016/0020-0190(93)90069-L.
Thomas Colcombet, Nathanaël Fijalkow, Pawel Gawrychowski, and Pierre Ohlmann. The theory of universal graphs for infinite duration games. CoRR, abs/2104.05262, 2021. arXiv: 2104.05262.
Thomas Colcombet, Nathanaël Fijalkow, and Florian Horn. Playing safe. In Venkatesh Raman and S. P. Suresh, editors, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014, December 15-17, 2014, New Delhi, India, volume 29 of LIPIcs, pages 379–390. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2014. doi:10.4230/LIPIcs.FSTTCS.2014.379.
Thomas Colcombet and Damian Niwiński. On the positional determinacy of edge-labeled games. Theor. Comput. Sci., 352(1-3):190–196, 2006. doi:10.1016/j.tcs.2005.10.046.
Stefan Dziembowski, Marcin Jurdzinski, and Igor Walukiewicz. How much memory is needed to win infinite games? In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 – July 2, 1997, pages 99–110. IEEE Computer Society, 1997. doi:10.1109/LICS.1997.614939.
Andrzej Ehrenfeucht and Jan Mycielski. Positional strategies for mean payoff games. Int. Journal of Game Theory, 8(2):109–113, 1979. doi:10.1007/BF01768705.
E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus and determinacy (extended abstract). In 32nd Annual Symposium on Foundations of Computer Science, San Juan, Puerto Rico, 1-4 October 1991, pages 368–377. IEEE Computer Society, 1991. doi:10.1109/SFCS.1991.185392.
Hugo Gimbert and Edon Kelmendi. Submixing and shift-invariant stochastic games. CoRR, abs/1401.6575, 2014. arXiv:1401.6575.
Hugo Gimbert and Wieslaw Zielonka. When can you play positionally? In Jirí Fiala, Václav Koubek, and Jan Kratochvíl, editors, Mathematical Foundations of Computer Science 2004, 29th International Symposium, MFCS 2004, Prague, Czech Republic, August 22-27, 2004, Proceedings, volume 3153 of Lecture Notes in Computer Science, pages 686–697. Springer, 2004. doi:10.1007/978-3-540-28629-5_53.
Hugo Gimbert and Wieslaw Zielonka. Games where you can play optimally without any memory. In Martín Abadi and Luca de Alfaro, editors, CONCUR 2005 – Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings, volume 3653 of Lecture Notes in Computer Science, pages 428–442. Springer, 2005. doi:10.1007/11539452_33.
Yuri Gurevich and Leo Harrington. Trees, automata, and games. In Harry R. Lewis, Barbara B. Simons, Walter A. Burkhard, and Lawrence H. Landweber, editors, Proceedings of the 14th Annual ACM Symposium on Theory of Computing, May 5-7, 1982, San Francisco, California, USA, pages 60–65. ACM, 1982. doi:10.1145/800070.802177.
Nils Klarlund. Progress measures, immediate determinacy, and a subset construction for tree automata. Ann. Pure Appl. Log., 69(2-3):243–268, 1994. doi:10.1016/0168-0072(94) 90086-8.
Nils Klarlund and Dexter C. Kozen. Rabin measures and their applications to fairness and automata theory. In LICS 1991, pages 256–265, 1991.
Eryk Kopczyński. Half-positional determinacy of infinite games. In Michele Bugliesi, Bart Preneel, Vladimiro Sassone, and Ingo Wegener, editors, Automata, Languages and Programming, 33rd International Colloquium, ICALP 2006, Venice, Italy, July 10-14, 2006, Proceedings, Part II, volume 4052 of Lecture Notes in Computer Science, pages 336–347. Springer, 2006. doi:10.1007/11787006_29.
Eryk Kopczyński. Omega-regular half-positional winning conditions. In Jacques Duparc and Thomas A. Henzinger, editors, Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings, volume 4646 of Lecture Notes in Computer Science, pages 41–53. Springer, 2007. doi:10.1007/978-3-540-74915-8_7.
Alexander Kozachinskiy. Energy games over totally ordered groups. CoRR, abs/2205.04508, 2022. doi:10.48550/arXiv.2205.04508.
Alexander Kozachinskiy. One-to-two-player lifting for mildly growing memory. In Petra Berenbrink and Benjamin Monmege, editors, 39th International Symposium on Theoretical Aspects of Computer Science, STACS 2022, March 15-18, 2022, Marseille, France (Virtual Conference), volume 219 of LIPIcs, pages 43:1–43:21. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022. doi:10.4230/LIPIcs.STACS.2022.43.
Denis Kuperberg and Michal Skrzypczak. On determinisation of good-for-games automata. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming – 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 299–310. Springer, 2015. doi:10.1007/978-3-662-47666-6_24.
Lawrence H. Landweber. Decision problems for omega-automata. Math. Syst. Theory, 3(4):376–384, 1969. doi:10.1007/BF01691063.
Stéphane Le Roux, Arno Pauly, and Mickael Randour. Extending finite-memory determinacy by Boolean combination of winning conditions. In Sumit Ganguly and Paritosh K. Pandya, editors, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018, December 11-13, 2018, Ahmedabad, India, volume 122 of LIPIcs, pages 38:1–38:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2018. doi: 10.4230/LIPIcs.FSTTCS.2018.38.
Oded Maler and Ludwig Staiger. On syntactic congruences for omega-languages. Theor. Comput. Sci., 183(1):93–112, 1997. doi:10.1016/S0304-3975(96)00312-X.
Robert McNaughton. Testing and generating infinite sequences by a finite automaton. Inf. Control., 9(5):521–530, 1966. doi:10.1016/S0019-9958(66)80013-X.
Andrzej Wlodzimierz Mostowski. Regular expressions for infinite trees and a standard form of automata. In Andrzej Skowron, editor, Computation Theory – Fifth Symposium, Zaborów, Poland, December 3-8, 1984, Proceedings, volume 208 of Lecture Notes in Computer Science, pages 157–168. Springer, 1984. doi:10.1007/3-540-16066-3_15.
A. Nerode. Linear automaton transformations. Proceedings of the American Mathematical Society, 9(4):541–544, 1958. doi:10.2307/2033204.
Pierre Ohlmann. Monotonic graphs for parity and mean-payoff games. PhD thesis, IRIF – Research Institute on the Foundations of Computer Science, 2021.
Dominique Perrin and Jean-Eric Pin. Infinite words – automata, semigroups, logic and games, volume 141 of Pure and applied mathematics series. Elsevier Morgan Kaufmann, 2004.
Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October – 1 November 1977, pages 46–57. IEEE Computer Society, 1977. doi:10.1109/SFCS.1977.32.
Amir Pnueli and Roni Rosner. On the synthesis of a reactive module. In POPL, pages 179–190, 1989. doi:10.1145/75277.75293.
Michael O. Rabin and Dana S. Scott. Finite automata and their decision problems. IBM J. Res. Dev., 3(2):114–125, 1959. doi:10.1147/rd.32.0114.
Lloyd S. Shapley. Stochastic games. Proceedings of the National Academy of Sciences, 39(10):1095–1100, 1953. doi:10.1073/pnas.39.10.1095.
Ludwig Staiger. Finite-state omega-languages. J. Comput. Syst. Sci., 27(3):434–448, 1983. doi:10.1016/0022-0000(83)90051-X.
Wolfgang Thomas. Church’s problem and a tour through automata theory. In Arnon Avron, Nachum Dershowitz, and Alexander Rabinovich, editors, Pillars of Computer Science, Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, volume 4800 of Lecture Notes in Computer Science, pages 635–655. Springer, 2008. doi:10.1007/ 978-3-540-78127-1_35.
Klaus Wagner. On ω-regular sets. Information and control, 43(2):123–177, 1979.
Wieslaw Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci., 200(1-2):135–183, 1998. doi:10.1016/S0304-3975(98) 00009-7.
