Reasoning About Additional Winning Strategies in Two-Player Games

  • Vadim MalvoneEmail author
  • Aniello Murano
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10767)


In game theory, deciding whether a designed player wins a game corresponds to check whether he has a winning strategy. There are situations in which it is important to know whether some extra winning strategy also exists. In this paper we investigate this question over two-player turn-based games under safety and fairness objectives. We provide an automata-based technique that allows to decide in polynomial-time whether the game admits more than one winning strategy.


  1. 1.
    Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Aminof, B., Malvone, V., Murano, A., Rubin, S.: Extended graded modalities in strategy logic. In: SR 2016, pp. 1–14 (2016)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Aminof, B., Malvone, V., Murano, A., Rubin, S.: Graded strategy logic: reasoning about uniqueness of nash equilibria. In: AAMAS 2016, pp. 698–706 (2016)Google Scholar
  4. 4.
    Aminof, B., Murano, A., Rubin, S.: On ctl* with graded path modalities. In: LPAR-20, pp. 281–296 (2015)CrossRefGoogle Scholar
  5. 5.
    Baader, F., Borgwardt, S., Lippmann, M.: Temporal conjunctive queries in expressive description logics with transitive roles. In: Pfahringer, B., Renz, J. (eds.) AI 2015. LNCS (LNAI), vol. 9457, pp. 21–33. Springer, Cham (2015). Scholar
  6. 6.
    Bianco, A., Mogavero, F., Murano, A.: Graded computation tree logic. Trans. Comput. Log. 13(3), 25:1–25:53 (2012)MathSciNetzbMATHGoogle Scholar
  7. 7.
    Bonatti, P., Lutz, C., Murano, A., Vardi, M.: The complexity of enriched mucalculi. Log. Methods Comput. Sci. 4(3), 1–27 (2008)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Bozzelli, L., Murano, A., Peron, A.: Pushdown module checking. Form. Methods Syst. Des. 36(1), 65–95 (2010)CrossRefGoogle Scholar
  9. 9.
    Chatterjee, K., Henzinger, M.: An O(n\({}^{\text{2}}\)) time algorithm for alternating büchi games. In: SODA 2012, pp. 1386–1399 (2012)Google Scholar
  10. 10.
    Simchi-Levi, D., Chen, X., Bramel, J.: The Logic of Logistics: Theory, Algorithms, and Applications for Logistics Management. SSORFE. Springer, New York (2014). Scholar
  11. 11.
    Ferrante, A., Murano, A., Parente, M.: Enriched mu-calculi module checking. Log. Methods Comput. Sci. 4(3), 1–21 (2008)MathSciNetzbMATHGoogle Scholar
  12. 12.
    Ferrante, A., Napoli, M., Parente, M.: Model checking for graded CTL. Fundam. Inf. 96(3), 323–339 (2009)MathSciNetzbMATHGoogle Scholar
  13. 13.
    Fraser, C.D.: The uniqueness of nash equilibrium in the private provision of public goods: an alternative proof. J. Publ. Econ. 49(3), 389–390 (1992)CrossRefGoogle Scholar
  14. 14.
    Gutierrez, J., Perelli, G., Wooldridge, M.: Iterated games with LDL goals over finite traces. In: AAMAS 2017, pp. 696–704 (2017)Google Scholar
  15. 15.
    Harel, D., Pnueli, A.: On the development of reactive systems. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems. NATO ASI Series (Series F: Computer and Systems Sciences), vol. 13. Springer, Heidelberg (1985). Scholar
  16. 16.
    Immerman, N.: Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sci. 22(3), 384–406 (1981)MathSciNetCrossRefGoogle Scholar
  17. 17.
    Jamroga, W., Murano, A.: On module checking and strategies. In: AAMAS 2014, pp. 701–708 (2014)Google Scholar
  18. 18.
    Jamroga, W., Murano, A.: Module checking of strategic ability. In: AAMAS 2015, pp. 227–235 (2015)Google Scholar
  19. 19.
    Kupferman, O., Sattler, U., Vardi, M.Y.: The complexity of the graded mu-calculus. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 423–437. Springer, Heidelberg (2002). Scholar
  20. 20.
    Kupferman, O., Vardi, M.Y.: Module checking revisited. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 36–47. Springer, Heidelberg (1997). Scholar
  21. 21.
    Kupferman, O., Vardi, M., Wolper, P.: An automata theoretic approach to branching-time model checking. J. ACM 47(2), 312–360 (2000)MathSciNetCrossRefGoogle Scholar
  22. 22.
    Kupferman, O., Vardi, M., Wolper, P.: Module checking. Inf. Comput. 164(2), 322–344 (2001)MathSciNetCrossRefGoogle Scholar
  23. 23.
    Malvone, V., Mogavero, F., Murano, A., Sorrentino, L.: Reasoning about graded strategy quantifiers. Inf. Comput. (to appear)Google Scholar
  24. 24.
    Malvone, V., Mogavero, F., Murano, A., Sorrentino, L.: On the counting of strategies. In: TIME 2015, pp. 170–179 (2015)Google Scholar
  25. 25.
    Malvone, V., Murano, A.: Additional winning strategies in two-player games. In: ICTCS 2016, pp. 251–256 (2016)Google Scholar
  26. 26.
    Malvone, V., Murano, A., Sorrentino, L.: Games with additional winning strategies. In: CILC 2015, pp. 175–180 (2015)Google Scholar
  27. 27.
    Mogavero, F., Murano, A., Perelli, G., Vardi, M.: Reasoning about strategies: on the model-checking problem. TOCL 15(4), 34:1–34:42 (2014)MathSciNetCrossRefGoogle Scholar
  28. 28.
    Murano, A., Perelli, G.: Pushdown multi-agent system verification. In: IJCAI 2015, pp. 1090–1097 (2015)Google Scholar
  29. 29.
    Murano, A., Sorrentino, L.: A game-based model for human-robots interaction. In: WOA 2015, pp. 146–150 (2015)Google Scholar
  30. 30.
    Papavassilopoulos, G., Cruz, J.B.: On the uniqueness of nash strategies for a class of analytic differential games. JOTA 27(2), 309–314 (1979)MathSciNetCrossRefGoogle Scholar
  31. 31.
    Pavel, L.: Game Theory for Control of Optical Networks. Springer, Heidelberg (2012). Scholar
  32. 32.
    Thomas, W.: Infinite trees and automaton definable relations over omega-words. In: STACS 1990, pp. 263–277 (1990)Google Scholar
  33. 33.
    Vardi, M.Y.: Alternating automata and program verification. In: van Leeuwen, J. (ed.) Computer Science Today. Lecture Notes in Computer Science, vol. 1000. Springer, Heidelberg (1995). Scholar
  34. 34.
    Wooldridge, M.: An Introduction to Multi Agent Systems. Wiley, Hoboken (2002)Google Scholar
  35. 35.
    Zhang, Y., Guizani, M.: Game Theory for Wireless Communications and Networking. CRC Press, Boca Raton (2011)zbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Université d’ÉvryÉvryFrance
  2. 2.Università degli Studi di Napoli Federico IINaplesItaly

Personalised recommendations