One-To-Two-Player Lifting for Mildly Growing Memory
We investigate a phenomenon of "one-to-two-player lifting" in infinite-duration two-player games on graphs with zero-sum objectives. More specifically, let 𝒞 be a class of strategies. It turns out that in many cases, to show that all two-player games on graphs with a given payoff function are determined in 𝒞, it is sufficient to do so for one-player games. That is, in many cases the determinacy in 𝒞 can be "lifted" from one-player games to two-player games. Namely, Gimbert and Zielonka (CONCUR 2005) have shown this for the class of positional strategies. Recently, Bouyer et al. (CONCUR 2020) have extended this to the classes of arena-independent finite-memory strategies. Informally, these are finite-memory strategies that use the same way of storing memory in all game graphs.
In this paper, we put the lifting technique into the context of memory complexity. The memory complexity of a payoff function measures, how many states of memory we need to play optimally in game graphs with up to n nodes, depending on n. We address the following question. Assume that we know the memory complexity of our payoff function in one-player games. Then what can be said about its memory complexity in two-player games? In particular, when is it finite?
In this paper, we answer this questions for strategies with "chromatic" memory. These are strategies that only accumulate sequences of colors of edges in their memory. We obtain the following results.
- Assume that the chromatic memory complexity in one-player games is sublinear in n on some infinite subsequence. Then the chromatic memory complexity in two-player games is finite.
- We provide an example in which (a) the chromatic memory complexity in one-player games is linear in n; (b) the memory complexity in two-player games is infinite. Thus, we obtain the exact barrier for the one-to-two-player lifting theorems in the setting of chromatic finite-memory strategies. Previous results only cover payoff functions with constant chromatic memory complexity.
Games on graphs
one-to-two-player lifting
strategy complexity
positional determinacy
finite-memory determinacy
Theory of computation~Logic
43:1-43:21
Regular Paper
This work was performed at the Steklov International Mathematical Center and supported by the Ministry of Science and Higher Education of the Russian Federation (agreement no. 075-15-2019-1614).
https://arxiv.org/abs/2104.13888
Alexander
Kozachinskiy
Alexander Kozachinskiy
Steklov Mathematical Institute of Russian Academy of Sciences, Moscow, Russia
https://orcid.org/0000-0002-9956-9023
10.4230/LIPIcs.STACS.2022.43
Paolo Baldan, Barbara König, Christina Mika-Michalski, and Tommaso Padoan. Fixpoint games on continuous lattices. Proceedings of the ACM on Programming Languages, 3(POPL):1-29, 2019.
Mikołaj Bojańczyk and Wojciech Czerwiński. An automata toolbox. A book of lecture notes, available at https://www.mimuw.edu.pl/∼bojan/upload/reduced-may-25.pdf, 2018.
Patricia Bouyer, Uli Fahrenberg, Kim G Larsen, Nicolas Markey, and Jiří Srba. Infinite runs in weighted timed automata with energy constraints. In International Conference on Formal Modeling and Analysis of Timed Systems, pages 33-47. Springer, 2008.
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 31st International Conference on Concurrency Theory (CONCUR 2020). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2020.
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), volume 203 of Leibniz International Proceedings in Informatics (LIPIcs), pages 26:1-26:18, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2021.26.
https://doi.org/10.4230/LIPIcs.CONCUR.2021.26
Patricia Bouyer, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove. Arena-independent finite-memory determinacy in stochastic games. arXiv preprint, 2021. URL: http://arxiv.org/abs/2102.10104.
http://arxiv.org/abs/2102.10104
J Richard Büchi and Lawrence H Landweber. Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society, 138:295-311, 1969.
Krishnendu Chatterjee and Laurent Doyen. Energy parity games. Theoretical Computer Science, 458:49-60, 2012.
Krishnendu Chatterjee, Mickael Randour, and Jean-François Raskin. Strategy synthesis for multi-dimensional quantitative objectives. Acta informatica, 51(3-4):129-163, 2014.
Andrzej Ehrenfeucht and Jan Mycielski. Positional strategies for mean payoff games. International Journal of Game Theory, 8(2):109-113, 1979.
E Allen Emerson and Charanjit S Jutla. Tree automata, mu-calculus and determinacy. In FoCS, volume 91, pages 368-377. Citeseer, 1991.
E Allen Emerson, Charanjit S Jutla, and A Prasad Sistla. On model-checking for fragments of μ-calculus. In International Conference on Computer Aided Verification, pages 385-396. Springer, 1993.
Hugo Gimbert and Wiesław Zielonka. Games where you can play optimally without any memory. In International Conference on Concurrency Theory, pages 428-442. Springer, 2005.
Hugo Gimbert and Wieslaw Zielonka. Pure and stationary optimal strategies in perfect-information stochastic games with global preferences. arXiv preprint, 2016. URL: http://arxiv.org/abs/1611.08487.
http://arxiv.org/abs/1611.08487
Erich Gradel and Wolfgang Thomas. Automata, logics, and infinite games: a guide to current research, volume 2500. Springer Science & Business Media, 2002.
Marcin Jurdziński, Ranko Lazić, and Sylvain Schmitz. Fixed-dimensional energy games are in pseudo-polynomial time. In International Colloquium on Automata, Languages, and Programming, pages 260-272. Springer, 2015.
Alexander Kozachinskiy. One-to-two-player lifting for mildly growing memory. arXiv preprint, 2021. URL: http://arxiv.org/abs/2104.13888.
http://arxiv.org/abs/2104.13888
Stéphane Le Roux. Time-aware uniformization of winning strategies. In Conference on Computability in Europe, pages 193-204. Springer, 2020.
Stéphane Le Roux and Arno Pauly. Extending finite-memory determinacy to multi-player games. Information and Computation, 261:676-694, 2018.
Stéphane Le Roux, Arno Pauly, and Mickael Randour. Extending finite-memory determinacy by boolean combination of winning conditions. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2018.
A Mostowski. Games with forbidden positions. Technical report, Preprint No. 78, Uniwersytet Gdanski, Instytyt Matematyki, 1991.
An A Muchnik. Games on infinite trees and automata with dead-ends: a new proof for the decidability of the monadic second order theory of two successors. Bulletin-European Association For Theoretical Computer Science, 48:219-219, 1992.
Wieslaw Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science, 200(1-2):135-183, 1998.
Uri Zwick and Mike Paterson. The complexity of mean payoff games on graphs. Theoretical Computer Science, 158(1-2):343-359, 1996.
Alexander Kozachinskiy
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode