Document Open Access Logo

A Look Back at Strategy Logic (Invited Contribution for the Test-of-Time Award)

Authors Krishnendu Chatterjee , Thomas A. Henzinger , Nir Piterman

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2026.6.pdf
  • Filesize: 0.49 MB
  • 7 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Verification by model checking
  • Theory of computation → Logic and verification
  • Theory of computation → Automata over infinite objects
Keywords
  • Strategy Logic
  • Games
  • Automata

Metrics

Abstract

In this note, we recall the history and our motivation behind the development of Strategy Logic and we discuss some of the work that ensued from its introduction.

Cite As Get BibTex

Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. A Look Back at Strategy Logic (Invited Contribution for the Test-of-Time Award). In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 6:1-6:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CONCUR.2026.6

Author Details

Krishnendu Chatterjee
  • ISTA, Klosterneuburg, Austria
Thomas A. Henzinger
  • ISTA, Klosterneuburg, Austria
Nir Piterman
  • University of Gothenburg and Chalmers University of Technology, Gothenburg, Sweden

Funding

  • Chatterjee, Krishnendu: Supported in part by the Austrian Science Fund (FWF) COE grant 10.55776/COE12 and the ERC CoG 863818 (ForM-SMArt).
  • Henzinger, Thomas A.: Supported in part by the ERC AdG 101020093 (VAMOS) and the FWF SFB grant F8502 (SPyCoDe).
  • Piterman, Nir: Supported in part by the Swedish research council (VR) project no. 2025-05419 and the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation.

Acknowledgements

We thank the jury that our paper introducing Strategy Logic at the Conference on Concurrency Theory (CONCUR) 2007 [Krishnendu Chatterjee et al., 2007] was chosen for a CONCUR Test-of-Time Award at CONCUR 2026.

References

  1. Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. Journal of the ACM, 49(5):672-713, 2002. URL: https://doi.org/10.1145/585265.585270.
  2. Benjamin Aminof, Marta Kwiatkowska, Bastien Maubert, Aniello Murano, and Sasha Rubin. Probabilistic strategy logic. In International Joint Conference on Artificial Intelligence (IJCAI), pages 32-38, 2019. URL: https://doi.org/10.24963/ijcai.2019/5.
  3. Benjamin Aminof, Vadim Malvone, Aniello Murano, and Sasha Rubin. Graded modalities in strategy logic. Information and Computation, 261:634-649, 2018. URL: https://doi.org/10.1016/j.ic.2018.02.022.
  4. Francesco Belardinelli, Wojciech Jamroga, Damian Kurpiewski, Vadim Malvone, and Aniello Murano. Strategy logic with simple goals: Tractable reasoning about strategies. In International Joint Conference on Artificial Intelligence (IJCAI), pages 88-94, 2019. URL: https://doi.org/10.24963/ijcai.2019/13.
  5. Raphaël Berthon, Bastien Maubert, Aniello Murano, Sasha Rubin, and Moshe Y. Vardi. Strategy logic with imperfect information. ACM Transactions on Computational Logic, 22(1):5:1-5:51, 2021. URL: https://doi.org/10.1145/3427955.
  6. Mikolaj Bojanczyk. A bounding quantifier. In Conference on Computer Science Logic (CSL), volume 3210 of Lecture Notes in Computer Science, pages 41-55. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30124-0_7.
  7. Patricia Bouyer, Romain Brenguier, Nicolas Markey, and Michael Ummels. Pure nash equilibria in concurrent deterministic games. Logical Methods in Computer Science, 11(2), 2015. URL: https://doi.org/10.2168/LMCS-11(2:9)2015.
  8. Patricia Bouyer, Nicolas Markey, and Daniel Stan. Mixed Nash equilibria in concurrent terminal-reward games. In Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS), volume 29 of LIPIcs, pages 351-363. Leibniz-Zentrum für Informatik, 2014. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2014.351.
  9. Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdzinski. Games with secure equilibria. Theoretical Computer Science, 365(1-2):67-82, 2006. URL: https://doi.org/10.1016/j.tcs.2006.07.032.
  10. Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Strategy logic. In Conference on Concurrency Theory (CONCUR), volume 4703 of Lecture Notes in Computer Science, pages 59-73. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74407-8_5.
  11. Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Strategy logic. Information and Computation, 208(6):677-693, 2010. URL: https://doi.org/10.1016/j.ic.2009.07.004.
  12. Edmund M. Clarke, E. Allen Emerson, and A. Prasad Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244-263, 1986. URL: https://doi.org/10.1145/5397.5399.
  13. Luca de Alfaro, Thomas A. Henzinger, and Orna Kupferman. Concurrent reachability games. Theoretical Computer Science, 386(3):188-217, 2007. URL: https://doi.org/10.1016/j.tcs.2007.07.008.
  14. Calvin C. Elgot and Michael O. Rabin. Decidability and undecidability of extensions of second (first) order theory of (generalized) successor. Journal of Symbolic Logic, 31(2):169-181, 1966. URL: https://doi.org/10.2307/2269808.
  15. E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus, and determinacy. In Symposium on Foundations of Computer Science (FOCS), pages 368-377. IEEE, 1991. URL: https://doi.org/10.1109/SFCS.1991.185392.
  16. Nathanaël Fijalkow, Bastien Maubert, Aniello Murano, and Sasha Rubin. Quantifying bounds in strategy logic. In Conference on Computer Science Logic (CSL), volume 119 of LIPIcs, pages 23:1-23:23. Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CSL.2018.23.
  17. Dana Fisman, Orna Kupferman, and Yoad Lustig. Rational synthesis. In Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 6015 of Lecture Notes in Computer Science, pages 190-204. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12002-2_16.
  18. Wojciech Jamroga, Damian Kurpiewski, and Vadim Malvone. Natural strategic abilities in voting protocols. In Workshop on Socio-Technical Aspects in Security and Trust (STAST), volume 12812 of Lecture Notes in Computer Science, pages 45-62. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-79318-0_3.
  19. François Laroussinie and Nicolas Markey. Augmenting ATL with strategy contexts. Information and Computation, 245:98-123, 2015. URL: https://doi.org/10.1016/j.ic.2014.12.020.
  20. Munyque Mittelmann, Bastien Maubert, Aniello Murano, and Laurent Perrussel. Automated synthesis of mechanisms. In International Joint Conference on Artificial Intelligence (IJCAI), pages 426-432. ijcai.org, 2022. URL: https://doi.org/10.24963/ijcai.2022/61.
  21. Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Y. Vardi. What makes ATL* decidable? A decidable fragment of strategy logic. In Conference on Concurrency Theory (CONCUR), volume 7454 of Lecture Notes in Computer Science, pages 193-208. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32940-1_15.
  22. Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Y. Vardi. Reasoning about strategies: On the model-checking problem. ACM Transactions on Computational Logic, 15(4):34:1-34:47, 2014. URL: https://doi.org/10.1145/2631917.
  23. Fabio Mogavero, Aniello Murano, and Luigi Sauro. On the boundary of behavioral strategies. In Symposium on Logic in Computer Science (LICS), pages 263-272. IEEE, 2013. URL: https://doi.org/10.1109/LICS.2013.32.
  24. Fabio Mogavero, Aniello Murano, and Moshe Y. Vardi. Reasoning about strategies. In Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 8 of LIPIcs, pages 133-144. Leibniz-Zentrum für Informatik, 2010. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2010.133.
  25. David E. Muller and Paul E. Schupp. Alternating automata on infinite trees. Theoretical Computer Science, 54:267-276, 1987. URL: https://doi.org/10.1016/0304-3975(87)90133-2.
  26. Gary L. Peterson and John H. Reif. Multiple-person alternation. In Symposium on Foundations of Computer Science (FOCS), pages 348-363. IEEE, 1979. URL: https://doi.org/10.1109/SFCS.1979.25.
  27. Gary L. Peterson, John H. Reif, and Salman Azhar. Lower bounds for multiplayer noncooperative games of incomplete information. Computers and Mathematics with Applications, 41:957-992, 2001. URL: https://doi.org/10.1016/S0898-1221(00)00333-3.
  28. Amir Pnueli. The temporal logic of programs. In Symposium on Foundations of Computer Science (FOCS), pages 46-57. IEEE Computer Society, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  29. Amir Pnueli and Roni Rosner. On the synthesis of a reactive module. In Symposium on Principles of Programming Languages (POPL), pages 179-190. ACM, 1989. URL: https://doi.org/10.1145/75277.75293.
  30. M.O. Rabin. Automata on infinite objects and Church’s problem. American Mathematical Society, 1972. URL: https://doi.org/10.1090/cbms/013.
  31. Michael Ummels and Dominik Wojtczak. The complexity of Nash equilibria in stochastic multiplayer games. Logical Methods in Computer Science, 7(3), 2011. URL: https://doi.org/10.2168/LMCS-7(3:20)2011.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact