Half-Positional Objectives Recognized by Deterministic Büchi Automata

[en] In two-player games on graphs, the simplest possible strategies are those that can be implemented without any memory. These are called positional strategies. In this paper, we characterize objectives recognizable by deterministic Büchi automata (a subclass of ω-regular objectives) that are half-positional, that is, for which the protagonist can always play optimally using positional strategies (both over 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

Disciplines :

Mathematics
Computer science

Author, co-author :

Bouyer, Patricia ; Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, Gif-sur-Yvette, France

Casares, Antonio ; LaBRI, Université de Bordeaux, Bordeaux, France

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 d'Informatique théorique ; Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, Gif-sur-Yvette, France

Language :

English

Title :

Half-Positional Objectives Recognized by Deterministic Büchi Automata

Publication date :

29 August 2024

Journal title :

Logical Methods in Computer Science

eISSN :

1860-5974

Publisher :

Logical Methods in Computer Science

Volume :

Issue :

Pages :

19:1-19:42

Peer reviewed :

Peer Reviewed verified by ORBi

Additional URL :

https://lmcs.episciences.org/14130/pdf

Research unit :

S820 - Mathématiques effectives

Research institute :

Complexys

Name of the research project :

5564 - ASPREN-Randour - FrontieRS - Fédération Wallonie Bruxelles
4743 - ASP-Vandenhove - FrontieRS - Fédération Wallonie Bruxelles
3284 - CQ-Randour - ManySynth - Fédération Wallonie Bruxelles

Funders :

F.R.S.-FNRS - Fonds de la Recherche Scientifique
ANR - Agence Nationale de la Recherche

Funding number :

ANR-20-CE25-0012

Funding text :

This work has been partially supported by the ANR Project MAVeriQ (ANR-20-CE25-0012). Mickael Randour is an F.R.S.-FNRS Research Associate and a member of the TRAIL Institute. Pierre Vandenhove was an F.R.S.-FNRS Research Fellow.

Available on ORBi UMONS :

since 13 September 2024

Statistics

Number of views

92 (4 by UMONS)

Number of downloads

22 (2 by UMONS)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

OpenAlex citations

Bibliography

[AF21] Dana Angluin and Dana Fisman. Regular ω-languages with an informative right congruence. Information and Computation, 278:104598, 2021. doi:10.1016/j.ic.2020.104598.
[AK22] Bader Abu Radi and Orna Kupferman. Minimization and canonization of GFG transition-based automata. Logical Methods in Computer Science, 18(3), 2022. doi:10.46298/lmcs-18(3:16)2022.
[AR17] Benjamin Aminof and Sasha Rubin. First-cycle games. Information and Computation, 254:195– 216, 2017. doi:10.1016/j.ic.2016.10.008.
[BCJ18] 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.
[BCRV22] Patricia Bouyer, Antonio Casares, Mickael Randour, and Pierre Vandenhove. Half-positional objectives recognized by deterministic Büchi automata. In Bartek Klin, S̷lawomir Lasota, and Anca Muscholl, editors, Proceedings of the 33rd International Conference on Concurrency Theory, CONCUR 2022, Warsaw, Poland, September 12–16, 2022, volume 243 of LIPIcs, pages 20:1–20:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022. doi:10.4230/LIPIcs.CONCUR.2022.20.
[BFL+ 08] 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, Proceedings of the 6th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2008, Saint Malo, France, September 15–17, 2008, volume 5215 of Lecture Notes in Computer Science, pages 33–47. Springer, 2008. doi:10.1007/978-3-540-85778-5_4.
[BFMM11] Alessandro Bianco, Marco Faella, Fabio Mogavero, and Aniello Murano. Exploring the boundary of half-positionality. Annals of Mathematics and Artificial Intelligence, 62(1-2):55–77, 2011. doi:10.1007/s10472-011-9250-1.
[BHR16] 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 7th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2016, Catania, Italy, September 14–16, 2016, volume 226 of EPTCS, pages 135–148, 2016. doi:10.4204/EPTCS.226.10.
[BHRR19] Véronique Bruyère, Quentin Hautem, Mickael Randour, and Jean-François Raskin. Energy mean-payoff games. In Wan J. Fokkink and Rob van Glabbeek, editors, Proceedings of the 30th International Conference on Concurrency Theory, CONCUR 2019, Amsterdam, the Netherlands, August 27–30, 2019, volume 140 of LIPIcs, pages 21:1–21:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2019. doi:10.4230/LIPIcs.CONCUR.2019.21.
[BK08] Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008.
[BL69] J. Richard Büchi and Lawrence H. Landweber. Definability in the monadic second-order theory of successor. Journal of Symbolic Logic, 34(2):166–170, 1969. doi:10.2307/2271090.
[BLO+ 22] Patricia Bouyer, Stéphane Le Roux, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove. Games where you can play optimally with arena-independent finite memory. Logical Methods in Computer Science, 18(1), 2022. doi:10.46298/lmcs-18(1:11)2022.
[BMR+ 18] Patricia Bouyer, Nicolas Markey, Mickael Randour, Kim G. Larsen, and Simon Laursen. Averageenergy games. Acta Informatica, 55(2):91–127, 2018. doi:10.1007/s00236-016-0274-1.
[Bok18] Udi Boker. Why these automata types? In Gilles Barthe, Geoff Sutcliffe, and Margus Veanes, editors, Proceedings of the 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2022, Awassa, Ethiopia, 16–21 November 2018, volume 57 of EPiC Series in Computing, pages 143–163. EasyChair, 2018. doi:10.29007/c3bj.
[BORV21] Patricia Bouyer, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove. Arenaindependent finite-memory determinacy in stochastic games. In Serge Haddad and Daniele Varacca, editors, Proceedings of the 32nd International Conference on Concurrency Theory, CONCUR 2021, Virtual Conference, August 24–27, 2021, volume 203 of LIPIcs, pages 26:1–26:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPIcs.CONCUR.2021.26.
[BRV23] Patricia Bouyer, Mickael Randour, and Pierre Vandenhove. Characterizing omega-regularity through finite-memory determinacy of games on infinite graphs. TheoretiCS, 2:1–48, 2023. doi:10.46298/theoretics.23.1.
[Büc62] J. Richard Büchi. On a decision method in restricted second order arithmetic. Proceedings of the International Congress on Logic, Methodology and Philosophy of Science, pages 1–11, 1962. doi:10.1007/978-1-4613-8928-6_23.
[Cas22] Antonio Casares. On the minimisation of transition-based Rabin automata and the chromatic memory requirements of Muller conditions. In Florin Manea and Alex Simpson, editors, Proceedings of the 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, Göttingen, Germany, February 14–19, 2022, volume 216 of LIPIcs, pages 12:1–12:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022. doi:10.4230/LIPIcs.CSL.2022.12.
[CCL22] 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 Miko̷laj Bojańczyk, Emanuela Merelli, and David P. Woodruff, editors, Proceedings of the 49th International Colloquium on Automata, Languages, and Programming, ICALP 2022, Paris, France, July 4–8, 2022, volume 229 of LIPIcs, pages 117:1–117:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022. doi:10.4230/LIPIcs.ICALP.2022.117.
[CD12] Krishnendu Chatterjee and Laurent Doyen. Energy parity games. Theoretical Computer Science, 458:49–60, 2012. doi:10.1016/j.tcs.2012.07.038.
[CDRR15] Krishnendu Chatterjee, Laurent Doyen, Mickael Randour, and Jean-François Raskin. Looking at mean-payoff and total-payoff through windows. Information and Computation, 242:25–52, 2015. doi:10.1016/j.ic.2015.03.010.
[CF13] Krishnendu Chatterjee and Nathanaël Fijalkow. Infinite-state games with finitary conditions. In Simona Ronchi Della Rocca, editor, Proceedings of the 27th International Workshop on Computer Science Logic, CSL 2013, 22nd Annual Conference of the EACSL, Torino, Italy, September 2–5, 2013, volume 23 of LIPIcs, pages 181–196. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2013. doi:10.4230/LIPIcs.CSL.2013.181.
[CFGO22] Thomas Colcombet, Nathanaël Fijalkow, Pawel Gawrychowski, and Pierre Ohlmann. The theory of universal graphs for infinite duration games. Logical Methods in Computer Science, 18(3), 2022. doi:10.46298/lmcs-18(3:29)2022.
[CFH14] Thomas Colcombet, Nathanaël Fijalkow, and Florian Horn. Playing safe. In Venkatesh Raman and S. P. Suresh, editors, Proceedings of the 34th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2014, New Delhi, India, December 15–17, 2014, volume 29 of LIPIcs, pages 379–390. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2014. doi:10.4230/LIPIcs.FSTTCS.2014.379.
[CHJ05] Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdziński. Mean-payoff parity games. In Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, LICS 2005, Chicago, IL, USA, June 26–29, 2005, pages 178–187. IEEE Computer Society, 2005. doi:10.1109/LICS.2005.26.
[CN06] Thomas Colcombet and Damian Niwiński. On the positional determinacy of edge-labeled games. Theoretical Computer Science, 352(1-3):190–196, 2006. doi:10.1016/j.tcs.2005.10.046.
[DJW97] Stefan Dziembowski, Marcin Jurdziński, and Igor Walukiewicz. How much memory is needed to win infinite games? In Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, LICS 1997, Warsaw, Poland, June 29 – July 2, 1997, pages 99–110. IEEE Computer Society, 1997. doi:10.1109/LICS.1997.614939.
[EJ91] E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus and determinacy (extended abstract). In Proceedings of the 32nd Annual Symposium on Foundations of Computer Science, FOCS 1991, San Juan, Puerto Rico, October, 1991, pages 368–377. IEEE Computer Society, 1991. doi:10.1109/SFCS.1991.185392.
[EM79] Andrzej Ehrenfeucht and Jan Mycielski. Positional strategies for mean payoff games. International Journal of Game Theory, 8(2):109–113, 1979. doi:10.1007/BF01768705.
[GH82] 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, STOC 1982, San Francisco, CA, USA, May 5–7, 1982, pages 60–65. ACM, 1982. doi:10.1145/800070.802177.
[GK14a] Hugo Gimbert and Edon Kelmendi. Submixing and shift-invariant stochastic games. CoRR, abs/1401.6575, 2014. doi:10.48550/arXiv.1401.6575.
[GK14b] Hugo Gimbert and Edon Kelmendi. Two-player perfect-information shift-invariant submixing stochastic games are half-positional. CoRR, abs/1401.6575v2, 2014. arXiv:1401.6575v2.
[GZ04] Hugo Gimbert and Wies̷law Zielonka. When can you play positionally? In Jiří Fiala, Václav Koubek, and Jan Kratochvíl, editors, Proceedings of the 29th International Symposium on Mathematical Foundations of Computer Science, MFCS 2004, Prague, Czech Republic, August 22–27, 2004, volume 3153 of Lecture Notes in Computer Science, pages 686–697. Springer, 2004. doi:10.1007/978-3-540-28629-5_53.
[GZ05] Hugo Gimbert and Wies̷law Zielonka. Games where you can play optimally without any memory. In Martín Abadi and Luca de Alfaro, editors, Proceedings of the 16th International Conference on Concurrency Theory, CONCUR 2005, San Francisco, CA, USA, August 23–26, 2005, volume 3653 of Lecture Notes in Computer Science, pages 428–442. Springer, 2005. doi:10.1007/11539452_33.
[Hor09] Florian Horn. Random fruits on the Zielonka tree. In Susanne Albers and Jean-Yves Marion, editors, Proceedings of the 26th International Symposium on Theoretical Aspects of Computer Science, STACS 2009, Freiburg, Germany, February 26–28, 2009, volume 3 of LIPIcs, pages 541–552. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Germany, 2009. doi:10.4230/LIPIcs.STACS.2009.1848.
[KK91] Nils Klarlund and Dexter Kozen. Rabin measures and their applications to fairness and automata theory. In Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science, LICS 1991, Amsterdam, The Netherlands, July 15–18, 1991, pages 256–265. IEEE Computer Society, 1991. doi:10.1109/LICS.1991.151650.
[Kla94] Nils Klarlund. Progress measures, immediate determinacy, and a subset construction for tree automata. Annals of Pure and Applied Logic, 69(2-3):243–268, 1994. doi:10.1016/0168-0072(94) 90086-8.
[Kop06] Eryk Kopczyński. Half-positional determinacy of infinite games. In Michele Bugliesi, Bart Preneel, Vladimiro Sassone, and Ingo Wegener, editors, Proceedings (Part II) of the 33rd International Colloquium on Automata, Languages and Programming, ICALP 2006, Venice, Italy, July 10– 14, 2006, volume 4052 of Lecture Notes in Computer Science, pages 336–347. Springer, 2006. doi:10.1007/11787006_29.
[Kop07] Eryk Kopczyński. Omega-regular half-positional winning conditions. In Jacques Duparc and Thomas A. Henzinger, editors, Proceedings of the 21st International Workshop on Computer Science Logic, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11–15, 2007, volume 4646 of Lecture Notes in Computer Science, pages 41–53. Springer, 2007. doi:10.1007/978-3-540-74915-8_7.
[Kop08] Eryk Kopczyński. Half-positional Determinacy of Infinite Games. PhD thesis, Warsaw University, 2008.
[Koz22a] Alexander Kozachinskiy. Energy games over totally ordered groups. CoRR, abs/2205.04508, 2022. doi:10.48550/arXiv.2205.04508.
[Koz22b] Alexander Kozachinskiy. One-to-two-player lifting for mildly growing memory. In Petra Berenbrink and Benjamin Monmege, editors, Proceedings of the 39th International Symposium on Theoretical Aspects of Computer Science, STACS 2022, Marseille, France, March 15–18, 2022, volume 219 of LIPIcs, pages 43:1–43:21. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022. doi:10.4230/LIPIcs.STACS.2022.43.
[KS15] 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, Proceedings (Part II) of the 42nd International Colloquium on Automata, Languages, and Programming, ICALP 2015, Kyoto, Japan, July 6–10, 2015, volume 9135 of Lecture Notes in Computer Science, pages 299–310. Springer, 2015. doi:10.1007/978-3-662-47666-6_24.
[Kur87] Robert P. Kurshan. Complementing deterministic Büchi automata in polynomial time. Journal of Computer and System Sciences, 35(1):59–71, 1987. doi:10.1016/0022-0000(87)90036-5.
[Lan69] Lawrence H. Landweber. Decision problems for omega-automata. Mathematical Systems Theory, 3(4):376–384, 1969. doi:10.1007/BF01691063.
[Le 90] Bertrand Le Saëc. Saturating right congruences. RAIRO – Theoretical Informatics and Applications, 24:545–559, 1990. doi:10.1051/ita/1990240605451.
[Löd01] Christof Löding. Efficient minimization of deterministic weak omega-automata. Information Processing Letters, 79(3):105–109, 2001. doi:10.1016/S0020-0190(00)00183-6.
[LPR18] 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, Proceedings of the 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018, Ahmedabad, India, December 11–13, 2018, volume 122 of LIPIcs, pages 38:1–38:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2018. doi:10.4230/LIPIcs.FSTTCS.2018.38.
[McN66] Robert McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9(5):521–530, 1966. doi:10.1016/S0019-9958(66)80013-X.
[Mos84] Andrzej W. Mostowski. Regular expressions for infinite trees and a standard form of automata. In Andrzej Skowron, editor, Proceedings of the 5th Symposium on Computation Theory, SCT 1984, Zaborów, Poland, December 3–8, 1984, volume 208 of Lecture Notes in Computer Science, pages 157–168. Springer, 1984. doi:10.1007/3-540-16066-3_15.
[MS97] Oded Maler and Ludwig Staiger. On syntactic congruences for omega-languages. Theoretical Computer Science, 183(1):93–112, 1997. doi:10.1016/S0304-3975(96)00312-X.
[Ner58] Anil Nerode. Linear automaton transformations. Proceedings of the American Mathematical Society, 9(4):541–544, 1958. doi:10.2307/2033204.
[Ohl21] Pierre Ohlmann. Monotonic graphs for parity and mean-payoff games. PhD thesis, IRIF – Research Institute on the Foundations of Computer Science, 2021.
[Ohl23] Pierre Ohlmann. Characterizing positionality in games of infinite duration over infinite graphs. TheoretiCS, 2:1–51, 2023. doi:10.46298/theoretics.23.3.
[Pnu77] Amir Pnueli. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science, FOCS 1977, Providence, RI, USA, October 31 – November 1, 1977, pages 46–57. IEEE Computer Society, 1977. doi:10.1109/SFCS.1977.32.
[PP04] 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.
[PR89] Amir Pnueli and Roni Rosner. On the synthesis of a reactive module. In Proceedings of the 16th Annual ACM Symposium on Principles of Programming Languages, POPL 1989, Austin, TX, USA, January 11–13, 1989, pages 179–190. ACM Press, 1989. doi:10.1145/75277.75293.
[Put94] Martin L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics. Wiley, 1994. doi:10.1002/9780470316887.
[RS59] Michael O. Rabin and Dana S. Scott. Finite automata and their decision problems. IBM Journal of Research and Development, 3(2):114–125, 1959. doi:10.1147/rd.32.0114.
[Sha53] Lloyd S. Shapley. Stochastic games. Proceedings of the National Academy of Sciences, 39(10):1095– 1100, 1953. doi:10.1073/pnas.39.10.1095.
[Sta83] Ludwig Staiger. Finite-state ω-languages. Journal of Computer and System Sciences, 27(3):434– 448, 1983. doi:10.1016/0022-0000(83)90051-X.
[Tar72] Robert E. Tarjan. Depth-first search and linear graph algorithms. SIAM Journal on Computing, 1(2):146–160, 1972. doi:10.1137/0201010.
[Tho08] 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.
[Wag79] Klaus W. Wagner. On ω-regular sets. Information and Control, 43(2):123–177, 1979. doi: 10.1016/S0019-9958(79)90653-3.
[Zie98] Wies̷law Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science, 200(1-2):135–183, 1998. doi:10.1016/S0304-3975(98) 00009-7.