Strategic Knowledge of the Past - Expressivity and Complexity

  • Christophe CharetonEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10767)


In this article we present theoretical results for an epistemic strategy logic with past operators, \(\text {PKSL}\). In \(\text {PKSL}\), agents are able to choose their strategies depending on past moves of other agents. This strictly extends the expressive power of some well-known epistemic strategy logics, which we illustrate by modelling forward induction: a rationality criterion, called admissibility, may be defined over agent’s strategies. Admissibility specifies coherence conditions between past and future actions, inducing new conditions for the availability of optimal strategies. We also give a resolution algorithm for \(\text {PKSL}\) model-checking. It runs in exponential time, while the satisfiability problem is undecidable, as is the case for similar logics for strategies such as Strategy Logic.



The author acknowledges financial support from ERC project EPS 313360 and thanks Hans van Ditmarsch for his useful comments on the presented research. He also gives thanks to the anonymous reviewers of conference SR 2017 for their comments on a previous version of this article.


  1. 1.
    Chatterjee, K., Henzinger, T.A., Piterman, N.: Strategy logic. Inf. Comp. 208(6), 677–693 (2010)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Mogavero, F., Murano, A., Perelli, G., Vardi, M.Y.: Reasoning about strategies: On the model-checking problem. ACM Trans. Comput. Log. 15(4), 1–47 (2014)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Ågotnes, T., Goranko, V., Jamroga, W., Wooldridge, M.: Knowledge and ability. Volume In: van Ditmarsch, H., Halpern, J.Y., van der Hoek, W., Kooi, B. (eds.) Handbook of Epistemic Logic, pp. 543–589. College Publications (2015)Google Scholar
  4. 4.
    Jamroga, W., Ågotnes, T.: Constructive knowledge: what agents can achieve under imperfect information. J. Appl. Non-Class. Log. 17, 423–475 (2007)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Belardinelli, F.: Reasoning about knowledge and strategies: epistemic strategy logic. In: Proceedings of 2nd International Workshop on Strategic Reasoning, SR, pp. 27–33 (2014)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Knight, S., Maubert, B.: Dealing with imperfect information in strategy logic. In: Proceedings of 3rd International Workshop on Strategic Reasoning, SR (2015)Google Scholar
  7. 7.
    Huang, X., van der Meyden, R.: An epistemic strategy logic. In: Proceedings of 2nd International Workshop on Strategic Reasoning, SR, pp. 35–41 (2014)Google Scholar
  8. 8.
    Van Ditmarsch, H., van Der Hoek, W., Kooi, B.: Dynamic Epistemic Logic, vol. 337. Springer Science & Business Media, Netherlands (2007). Scholar
  9. 9.
    Chareton, C., van Ditmarsch, H.: Strategic knowledge of the past in quantum cryptography. In: Baltag, A., Seligman, J., Yamada, T. (eds.) LORI 2017. LNCS, vol. 10455, pp. 347–361. Springer, Heidelberg (2017). Scholar
  10. 10.
    Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 196–218. Springer, Heidelberg (1985). Scholar
  11. 11.
    Vardi, M.Y.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 628–641. Springer, Heidelberg (1998). Scholar
  12. 12.
    French, T., van der Meyden, R., Reynolds, M.: Axioms for logics of knowledge and past time: synchrony and unique initial states. In: Proceedings of AiML, vol. 5, pp. 53–72 (2004)Google Scholar
  13. 13.
    Sack, J.: Logic for update products and steps into the past. Ann. Pure Appl. Logic 161(12), 1431–1461 (2010)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Guelev, D.P., Dima, C.: Model-checking strategic ability and knowledge of the past of communicating coalitions. In: Baldoni, M., Son, T.C., van Riemsdijk, M.B., Winikoff, M. (eds.) DALT 2008. LNCS (LNAI), vol. 5397, pp. 75–90. Springer, Heidelberg (2009). Scholar
  15. 15.
    Skyrms, B.: The Stag Hunt and the Evolution of Social Structure. Cambridge University Press, Cambridge (2004)Google Scholar
  16. 16.
    Brenguier, R., Pérez, G.A., Raskin, J.F., Sankur, O.: Admissibility in quantitative graph games. arXiv preprint arXiv:1611.08677 (2016)
  17. 17.
    Berwanger, D.: Admissibility in infinite games. In: Thomas, W., Weil, P. (eds.) STACS 2007. LNCS, vol. 4393, pp. 188–199. Springer, Heidelberg (2007). Scholar
  18. 18.
    Van Damme, E.: Stable equilibria and forward induction. J. Econ. Theory 48(2), 476–496 (1989)MathSciNetCrossRefGoogle Scholar
  19. 19.
    Cooper, R., De Jong, D.V., Forsythe, R., Ross, T.W.: Forward induction in coordination games. Econ. Lett. 40(2), 167–172 (1992)CrossRefGoogle Scholar
  20. 20.
    Chareton, C., Brunel, J., Chemouil, D.: Towards an updatable strategy logic. In: Proceedings of 1st International Workshop on Strategic Reasoning, SR, pp. 91–98 (2013)MathSciNetCrossRefGoogle Scholar
  21. 21.
    Chareton, C., Brunel, J., Chemouil, D.: A logic with revocable and refinable strategies. Inf. Comput. 242, 157–182 (2015)MathSciNetCrossRefGoogle Scholar
  22. 22.
    De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Proceedings of 22th IJCAI, pp. 854–860 (2013)Google Scholar
  23. 23.
    Baltag, A.: A logic for suspicious players: Epistemic actions and belief-updates in games. Technical report, Amsterdam, The Netherlands (2000)Google Scholar
  24. 24.
    Chandra, A.K., Stockmeyer, L.J.: Alternation. In: 17th Annual Symposium on Foundations of Computer Science, pp. 98–108. IEEE (1976)Google Scholar
  25. 25.
    Harel, D.: Recurring dominoes: making the highly undecidable highly understandable. North-Holl. Math. Stud. 102, 51–71 (1985)MathSciNetCrossRefGoogle Scholar
  26. 26.
    Mogavero, F., Murano, A., Perelli, G., Vardi, M.Y.: Reasoning about strategies: on the satisfiability problem. Log. Methods Comput. Sci. 13(1), 1–37 (2017)MathSciNetzbMATHGoogle Scholar
  27. 27.
    Čermák, P., Lomuscio, A., Mogavero, F., Murano, A.: MCMAS-SLK: a model checker for the verification of strategy logic specifications. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 525–532. Springer, Cham (2014). Scholar
  28. 28.
    Belardinelli, F., Lomuscio, A., Murano, A., Rubin, S.: Verification of broadcasting multi-agent systems against an epistemic strategy logic. In: Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19–25, 2017, pp. 91–97 (2017)Google Scholar
  29. 29.
    Berthon, R., Maubert, B., Murano, A., Rubin, S., Vardi, M.Y.: Strategy logic with imperfect information. In: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20–23, 2017, pp. 1–12 (2017)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.LORIA, CNRS, Université de LorraineLorraineFrance

Personalised recommendations