Document

# Optimal Strategies in Concurrent Reachability Games

## File

LIPIcs.CSL.2022.7.pdf
• Filesize: 1.08 MB
• 17 pages

## Cite As

Benjamin Bordais, Patricia Bouyer, and Stéphane Le Roux. Optimal Strategies in Concurrent Reachability Games. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CSL.2022.7

## Abstract

We study two-player reachability games on finite graphs. At each state the interaction between the players is concurrent and there is a stochastic Nature. Players also play stochastically. The literature tells us that 1) Player 𝖡, who wants to avoid the target state, has a positional strategy that maximizes the probability to win (uniformly from every state) and 2) from every state, for every ε > 0, Player 𝖠 has a strategy that maximizes up to ε the probability to win. Our work is two-fold. First, we present a double-fixed-point procedure that says from which state Player 𝖠 has a strategy that maximizes (exactly) the probability to win. This is computable if Nature’s probability distributions are rational. We call these states maximizable. Moreover, we show that for every ε > 0, Player 𝖠 has a positional strategy that maximizes the probability to win, exactly from maximizable states and up to ε from sub-maximizable states. Second, we consider three-state games with one main state, one target, and one bin. We characterize the local interactions at the main state that guarantee the existence of an optimal Player 𝖠 strategy. In this case there is a positional one. It turns out that in many-state games, these local interactions also guarantee the existence of a uniform optimal Player 𝖠 strategy. In a way, these games are well-behaved by design of their elementary bricks, the local interactions. It is decidable whether a local interaction has this desirable property.

## Subject Classification

##### ACM Subject Classification
• Theory of computation → Solution concepts in game theory
##### Keywords
• Concurrent reachability games
• Game forms
• Optimal strategies

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. Roderick Bloem, Krishnendu Chatterjee, and Barbara Jobstmann. Handbook of Model Checking, chapter Graph games and reactive synthesis, pages 921-962. Springer, 2018.
2. Benjamin Bordais, Patricia Bouyer, and Stéphane Le Roux. From local to global determinacy in concurrent graph games. Technical Report abs/2107.04081, CoRR, 2021. URL: http://arxiv.org/abs/2107.04081.
3. Benjamin Bordais, Patricia Bouyer, and Stéphane Le Roux. Optimal strategies in concurrent reachability games. CoRR, abs/2110.14724, 2021. URL: http://arxiv.org/abs/2110.14724.
4. Krishnendu Chatterjee, Marcin Jurdziński, and Thomas A. Henzinger. Quantitative stochastic parity games. In Proc. of 15th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA'04), pages 121-130. SIAM, 2004.
5. Luca de Alfaro. Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, 1997.
6. Luca de Alfaro, Thomas Henzinger, and Orna Kupferman. Concurrent reachability games. Theoretical Computer Science, 386(3):188-217, 2007.
7. Luca de Alfaro and Rupak Majumdar. Quantitative solution of omega-regular games. Journal of Computer and System Sciences, 68:374-397, 2004.
8. Hugh Everett. Recursive games. Annals of Mathematics Studies - Contributions to the Theory of Games, 3:67-78, 1957.
9. Jerzy Filar and Koos Vrieze. Competitive Markov decision processes. Springer Science & Business Media, 2012.
10. Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Patrick Totzke. Strategy complexity of parity objectives in countable mdps. In Proc. 31st International Conference on Concurrency Theory (CONCUR'20), volume 171 of LIPIcs, pages 39:1-39:17. Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.39.
11. Elon Kohlberg. Repeated games with absorbing states. The Annals of Statistics, pages 724-738, 1974.
12. Antonín Kučera. Lectures in Game Theory for Computer Scientists, chapter Turn-Based Stochastic Games, pages 146-184. Cambridge University Press, 2011.
13. Donald A. Martin. The determinacy of blackwell games. The Journal of Symbolic Logic, 63(4):1565-1581, 1998.
14. Annabelle McIver and Carroll Morgan. Games, probability and the quantitative μ-calculus qmμ. In Proc. 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'02), volume 2514 of Lecture Notes in Computer Science, pages 292-310. Springer, 2002.
15. James Renegar. On the computational complexity and geometry of the first-order theory of the reals. part iii: Quantifier elimination. Journal of Symbolic Computation, 13(3):329-352, 1992. URL: https://doi.org/10.1016/S0747-7171(10)80005-7.
16. Wolfgang Thomas. Infinite games and verification. In Proc. 14th International Conference on Computer Aided Verification (CAV'02), volume 2404 of Lecture Notes in Computer Science, pages 58-64. Springer, 2002. Invited Tutorial.
17. Moshe Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proc. 26th Annual Symposium on Foundations of Computer Science (FOCS'85), pages 327-338. IEEE Computer Society Press, 1985.
18. John von Neumann and Oskar Morgenstern. Theory of Games and Economic Behavior. Princeton Univ. Press, Princeton, 1944.
19. Wiesław Zielonka. Perfect-information stochastic parity games. In Proc. 7th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'04), volume 2987 of Lecture Notes in Computer Science, pages 499-513. Springer, 2004.
X

Feedback for Dagstuhl Publishing