Half-Positional Objectives Recognized by Deterministic Büchi Automata (Extended Abstract)

[en] In two-player zero-sum games on graphs, the protagonist tries to achieve an objective while the antagonist aims to prevent it. Objectives for which both players do not need to use memory to play optimally are well-understood and characterized both in finite and infinite graphs. Less is known about the larger class of half-positional objectives, i.e., those for which the protagonist does not need memory (but for which the antagonist might). In particular, no characterization of half-positionality is known for the central class of ω-regular objectives. Here, we characterize objectives recognizable by deterministic Büchi automata (a class of ω-regular objectives) that are half-positional, both over finite and infinite graphs. 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 [FR] > Laboratoire Méthodes Formelles (LMF)

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 [FR] > Laboratoire Méthodes Formelles (LMF)

Language :

English

Title :

Half-Positional Objectives Recognized by Deterministic Büchi Automata (Extended Abstract)

Publication date :

August 2023

Event name :

International Joint Conference on Artificial Intelligence (IJCAI 2023)

Event place :

Macao, Macao SAR China

Event date :

19th-25th August 2023

Event number :

By request :

Yes

Audience :

International

Journal title :

IJCAI - International Joint Conference on Artificial Intelligence

ISSN :

10450823

Peer reviewed :

Peer reviewed

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
5727 - PDR-Randour - ControlleRS

Funders :

F.R.S.-FNRS - Fonds de la Recherche Scientifique [BE]

Funding text :

This work has been supported by the ANR Project MAVeriQ (ANR-20-CE25-0012) and by the Fonds de la Recherche Scientifique - FNRS under Grant n° T.0188.23 (PDR ControlleRS). 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.

Available on ORBi UMONS :

since 14 August 2023

Statistics

Number of views

14 (9 by UMONS)

Number of downloads

2 (1 by UMONS)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

Bibliography

Benjamin Aminof and Sasha Rubin. First-cycle games. Inf. Comput., 254:195-216, 2017.
Dana Angluin and Dana Fisman. Regular ω-languages with an informative right congruence. Inf. Comput., 278:104598, 2021.
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.
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.
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, FORMATS 2008, volume 5215 of Lect. Notes Comput. Sci., pages 33-47. Springer, 2008.
Patricia Bouyer, Nicolas Markey, Mickael Randour, Kim G. Larsen, and Simon Laursen. Average-energy games. Acta Inform., 55(2):91-127, 2018.
Patricia Bouyer, Antonio Casares, Mickael Randour, and Pierre Vandenhove. Half-positional objectives recognized by deterministic Büchi automata. In Bartek Klin, Sławomir Lasota, and Anca Muscholl, editors, CONCUR 2022, volume 243 of LIPIcs, pages 20:1-20:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.
Patricia Bouyer, Stéphane Le Roux, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove. Games where you can play optimally with arena-independent finite memory. Log. Methods Comput. Sci., 18(1), 2022.
Patricia Bouyer, Mickael Randour, and Pierre Vandenhove. The true colors of memory: A tour of chromatic-memory strategies in zero-sum games on graphs (invited talk). In Anuj Dawar and Venkatesan Guruswami, editors, FSTTCS 2022, volume 250 of LIPIcs, pages 3:1-3:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.
Patricia Bouyer, Nathanaël Fijalkow, Mickael Randour, and Pierre Vandenhove. How to play optimally for regular objectives? In ICALP 2023 (to appear), volume 261 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.
Patricia Bouyer, Mickael Randour, and Pierre Vandenhove. Characterizing omega-regularity through finite-memory determinacy of games on infinite graphs. TheoretiCS, 2:1-48, 2023.
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.
J. Richard Büchi. On a decision method in restricted second order arithmetic. International Congress on Logic, Methodology and Philosophy of Science, pages 1-11, 1962.
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łaj Bojańczyk, Emanuela Merelli, and David P. Woodruff, editors, ICALP 2022, volume 229 of LIPIcs, pages 117:1-117:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.
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, CSL 2022, volume 216 of LIPIcs, pages 12:1-12:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.
Krishnendu Chatterjee and Laurent Doyen. Energy parity games. Theor. Comput. Sci., 458:49-60, 2012.
Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdziński. Mean-payoff parity games. In LICS 2005, pages 178-187. IEEE Computer Society, 2005.
Thomas Colcombet and Damian Niwiński. On the positional determinacy of edge-labeled games. Theor. Comput. Sci., 352(1-3):190-196, 2006.
Thomas Colcombet, Nathanaël Fijalkow, and Florian Horn. Playing safe. In Venkatesh Ra-man and S. P. Suresh, editors, FSTTCS 2014, volume 29 of LIPIcs, pages 379-390. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014.
Stefan Dziembowski, Marcin Jurdziński, and Igor Walukiewicz. How much memory is needed to win infinite games? In LICS 1997, pages 99-110. IEEE Computer Society, 1997.
Andrzej Ehrenfeucht and Jan Mycielski. Positional strategies for mean payoff games. Int. J. Game Theory, 8(2):109-113, 1979.
E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus and determinacy (extended abstract). In FOCS 1991, pages 368-377. IEEE Computer Society, 1991.
Nathanaël Fijalkow, Nathalie Bertrand, Patricia Bouyer-Decitre, Romain Brenguier, Arnaud Carayol, John Fearnley, Hugo Gimbert, Florian Horn, Rasmus Ibsen-Jensen, Nicolas Markey, Benjamin Monmege, Petr Novotný, Mickael Randour, Ocan Sankur, Sylvain Schmitz, Olivier Serre, and Mateusz Skomra. Games on Graphs. Online, 2023.
Hugo Gimbert and Wiesław Zielonka. When can you play positionally? In Jiří Fiala, Václav Koubek, and Jan Kratochvíl, editors, MFCS 2004, volume 3153 of Lect. Notes Comput. Sci., pages 686-697. Springer, 2004.
Hugo Gimbert and Wiesław Zielonka. Games where you can play optimally without any memory. In Martín Abadi and Luca de Alfaro, editors, CONCUR 2005, volume 3653 of Lect. Notes Comput. Sci., pages 428-442. Springer, 2005.
Yuri Gurevich and Leo Harrington. Trees, automata, and games. In Harry R. Lewis, Barbara B. Simons, Walter A. Burkhard, and Lawrence H. Landweber, editors, STOC 1982, pages 60-65. ACM, 1982.
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak. Alternating good-for-MDPs automata. In Ahmed Bouajjani, Lukás Holík, and Zhilin Wu, editors, ATVA 2022, volume 13505 of Lect. Notes Comput. Sci., pages 303-319. Springer, 2022.
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak. An impossibility result in automata-theoretic reinforcement learning. In Ahmed Bouajjani, Lukás Holík, and Zhilin Wu, editors, ATVA 2022, volume 13505 of Lect. Notes Comput. Sci., pages 42-57. Springer, 2022.
Nils Klarlund and Dexter Kozen. Rabin measures and their applications to fairness and automata theory. In LICS 1991, pages 256-265. IEEE Computer Society, 1991.
Nils Klarlund. Progress measures, immediate determinacy, and a subset construction for tree automata. Ann. Pure Appl. Log., 69(2-3):243-268, 1994.
Eryk Kopczyński. Half-positional determinacy of infinite games. In Michele Bugliesi, Bart Preneel, Vladimiro Sassone, and Ingo Wegener, editors, ICALP 2006, volume 4052 of Lect. Notes Comput. Sci., pages 336-347. Springer, 2006.
Eryk Kopczyński. Omega-regular half-positional winning conditions. In Jacques Duparc and Thomas A. Henzinger, editors, CSL 2007, volume 4646 of Lect. Notes Comput. Sci., pages 41-53. Springer, 2007.
Eryk Kopczyński. Half-positional Determinacy of Infinite Games. PhD thesis, Warsaw University, 2008.
Alexander Kozachinskiy. One-to-two-player lifting for mildly growing memory. In Petra Berenbrink and Benjamin Monmege, editors, STACS 2022, volume 219 of LIPIcs, pages 43:1-43:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.
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, FSTTCS 2018, volume 122 of LIPIcs, pages 38:1-38:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.
Bertrand Le Saëc. Saturating right congruences. RAIRO - Theoretical Informatics and Applications, 24:545-559, 1990.
Oded Maler and Ludwig Staiger. On syntactic congruences for omega-languages. Theor. Comput. Sci., 183(1):93-112, 1997.
Robert McNaughton. Testing and generating infinite sequences by a finite automaton. Inf. Control, 9(5):521-530, 1966.
Andrzej W. Mostowski. Regular expressions for infinite trees and a standard form of automata. In Andrzej Skowron, editor, SCT 1984, volume 208 of Lect. Notes Comput. Sci., pages 157-168. Springer, 1984.
Anil Nerode. Linear automaton transformations. Proc. Am. Math. Soc., 9(4):541-544, 1958.
Pierre Ohlmann. Characterizing positionality in games of infinite duration over infinite graphs. TheoretiCS, 2:1-51, 2023.
Amir Pnueli. The temporal logic of programs. In FOCS 1977, pages 46-57. IEEE Computer Society, 1977.
Lloyd S. Shapley. Stochastic games. Proc. Natl. Acad. Sci., 39(10):1095-1100, 1953.
Ludwig Staiger. Finite-state ω-languages. J. Comput. Syst. Sci., 27(3):434-448, 1983.
Richard S. Sutton and Andrew G. Barto. Reinforcement Learning: An Introduction. The MIT Press, second edition, 2018.
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 Lect. Notes Comput. Sci., pages 635-655. Springer, 2008.
Klaus W. Wagner. On ω-regular sets. Inf. Control, 43(2):123-177, 1979.
Wiesław Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci., 200(1-2):135-183, 1998.