A Game of Pawns

Authors Guy Avni , Pranav Ghorpade, Shibashis Guha

Thumbnail PDF


  • Filesize: 0.76 MB
  • 17 pages

Document Identifiers

Author Details

Guy Avni
  • University of Haifa, Israel
Pranav Ghorpade
  • Chennai Mathematical Institute, India
Shibashis Guha
  • Tata Institute of Fundamental Research, Mumbai, India

Cite AsGet BibTex

Guy Avni, Pranav Ghorpade, and Shibashis Guha. A Game of Pawns. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


We introduce and study pawn games, a class of two-player zero-sum turn-based graph games. A turn-based graph game proceeds by placing a token on an initial vertex, and whoever controls the vertex on which the token is located, chooses its next location. This leads to a path in the graph, which determines the winner. Traditionally, the control of vertices is predetermined and fixed. The novelty of pawn games is that control of vertices changes dynamically throughout the game as follows. Each vertex of a pawn game is owned by a pawn. In each turn, the pawns are partitioned between the two players, and the player who controls the pawn that owns the vertex on which the token is located, chooses the next location of the token. Control of pawns changes dynamically throughout the game according to a fixed mechanism. Specifically, we define several grabbing-based mechanisms in which control of at most one pawn transfers at the end of each turn. We study the complexity of solving pawn games, where we focus on reachability objectives and parameterize the problem by the mechanism that is being used and by restrictions on pawn ownership of vertices. On the positive side, even though pawn games are exponentially-succinct turn-based games, we identify several natural classes that can be solved in PTIME. On the negative side, we identify several EXPTIME-complete classes, where our hardness proofs are based on a new class of games called Lock & Key games, which may be of independent interest.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • Graph games
  • Reachability games
  • Pawn games
  • Dynamic vertex control


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


  1. M. Aghajohari, G. Avni, and T. A. Henzinger. Determinacy in discrete-bidding infinite-duration games. Log. Methods Comput. Sci., 17(1), 2021. Google Scholar
  2. P. Alizadeh Alamdari, G. Avni, T. A. Henzinger, and A. Lukina. Formal methods with a touch of magic. In Proc. 20th FMCAD, 2020. Google Scholar
  3. S. Almagor, G. Avni, and O. Kupferman. Repairing multi-player games. In Proc. 26th CONCUR, pages 325-339, 2015. Google Scholar
  4. R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672-713, 2002. Google Scholar
  5. K.R. Apt and E. Grädel. Lectures in Game Theory for Computer Scientists. Cambridge University Press, 2011. Google Scholar
  6. G. Avni, R. Bloem, K. Chatterjee, T. A. Henzinger, B. Könighofer, and S. Pranger. Run-time optimization for learned controllers through quantitative games. In Proc. 31st CAV, pages 630-649, 2019. Google Scholar
  7. G. Avni, P. Ghorpade, and S. Guha. A game of pawns. CoRR, abs/2305.04096, 2023. URL: https://arxiv.org/abs/2305.04096.
  8. G. Avni, T. A. Henzinger, and V. Chonev. Infinite-duration bidding games. J. ACM, 66(4):31:1-31:29, 2019. Google Scholar
  9. G. Avni and S. Sadhukhan. Computing threshold budgets in discrete-bidding games. In Proc. 42nd FSTTCS, volume 250 of LIPIcs, pages 30:1-30:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. Google Scholar
  10. G. Bielous and O. Kupferman. Coverage and vacuity in network formation games. In Proc. 28th CSL, 2020. Google Scholar
  11. R. Brenguier, L. Clemente, P. Hunter, G. A. Pérez, M. Randour, J.-F. Raskin, O. Sankur, and M. Sassolas. Non-zero sum games for reactive synthesis. In Proc. 10th LATA, pages 3-23, 2016. Google Scholar
  12. L. Brice, J.-F. Raskin, and M. van den Bogaard. Subgame-perfect equilibria in mean-payoff games. In In Proc. 32nd CONCUR, volume 203 of LIPIcs, pages 8:1-8:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  13. D. Busatto-Gaston, D. Chakraborty, S. Guha, G. A. Pérez, and J-F. Raskin. Safe learning for near-optimal scheduling. In QEST, Proceedings, volume 12846 of Lecture Notes in Computer Science, pages 235-254. Springer, 2021. Google Scholar
  14. P. Cerný, E. M. Clarke, T. A. Henzinger, A. Radhakrishna, L. Ryzhyk, R. Samanta, and T. Tarrach. From non-preemptive to preemptive scheduling using synchronization synthesis. Formal Methods Syst. Des., 50(2-3):97-139, 2017. Google Scholar
  15. K. Chatterjee, T. A. Henzinger, and N. Piterman. Strategy logic. Inf. Comput., 208(6):677-693, 2010. Google Scholar
  16. M. Develin and S. Payne. Discrete bidding games. The Electronic Journal of Combinatorics, 17(1):R85, 2010. Google Scholar
  17. D. Fisman, O. Kupferman, and Y. Lustig. Rational synthesis. In Proc. 16th TACAS, pages 190-204, 2010. Google Scholar
  18. E. Grädel, W. Thomas, and T. Wilke. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of Lecture Notes in Computer Science. Springer, 2002. Google Scholar
  19. B. Könighofer, M. Alshiekh, R. Bloem, L. Humphrey, R. Könighofer, U. Topcu, and C. Wang. Shield synthesis. Formal Methods in System Design, 51(2):332-361, 2017. Google Scholar
  20. O. Kupferman, G. Perelli, and M. Y. Vardi. Synthesis with rational environments. Ann. Math. Artif. Intell., 78(1):3-20, 2016. Google Scholar
  21. L. Lamport, R. E. Shostak, and M. C. Pease. The byzantine generals problem. ACM Trans. Program. Lang. Syst., 4(3):382-401, 1982. Google Scholar
  22. A. J. Lazarus, D. E. Loeb, J. G. Propp, W. R. Stromquist, and D. H. Ullman. Combinatorial games under auction play. Games and Economic Behavior, 27(2):229-264, 1999. Google Scholar
  23. F. Mogavero, A. Murano, G. Perelli, and M. Y. Vardi. Reasoning about strategies: On the model-checking problem. ACM Trans. Comput. Log., 15(4):34:1-34:47, 2014. Google Scholar
  24. F. Mogavero, A. Murano, and M. Y. Vardi. Reasoning about strategies. In Proc. 30th FSTTCS, pages 133-144, 2010. Google Scholar
  25. G. Perelli. Enforcing equilibria in multi-agent systems. In In Proc. 18th AAMAS, pages 188-196. International Foundation for Autonomous Agents and Multiagent Systems, 2019. Google Scholar
  26. A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proc. 16th POPL, pages 179-190, 1989. Google Scholar
  27. S. A. Seshia, N. Sharygina, and S. Tripakis. Modeling for verification. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 75-105. Springer, 2018. Google Scholar
  28. Michael Sipser. Introduction to the Theory of Computation. Course Technology, Boston, MA, 2013. Google Scholar
  29. R. S. Sutton and A. G. Barto. Reinforcement learning - An introduction. Adaptive computation and machine learning. MIT Press, 1998. Google Scholar
  30. M. Ummels. Stochastic multiplayer games: theory and algorithms. PhD thesis, RWTH Aachen University, 2011. Google Scholar
  31. J. van Benthem. An essay on sabotage and obstruction. In Mechanizing Mathematical Reasoning, Essays in Honor of Jörg H. Siekmann on the Occasion of His 60th Birthday, pages 268-276, 2005. Google Scholar
  32. M. J. Wooldridge, J. Gutierrez, P. Harrenstein, E. Marchioni, G. Perelli, and A. Toumi. Rational verification: From model checking to equilibrium checking. In Proc. of the 30th AAAI, pages 4184-4191, 2016. Google Scholar