Computer Aided Synthesis: A Game-Theoretic Approach

  • Véronique BruyèreEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10396)


In this invited contribution, we propose a comprehensive introduction to game theory applied in computer aided synthesis. In this context, we give some classical results on two-player zero-sum games and then on multi-player non zero-sum games. The simple case of one-player games is strongly related to automata theory on infinite words. All along the article, we focus on general approaches to solve the studied problems, and we provide several illustrative examples as well as intuitions on the proofs.


Games played on graphs Boolean objective Quantitative objective Winning strategy Nash Equilibrium Synthesis 



We would like to thank Patricia Bouyer, Thomas Brihaye, Emmanuel Filiot, Hugo Gimbert, Quentin Hautem, Mickaël Randour, and Jean-François Raskin for their useful discussions and comments that helped us to improve the presentation of this article.


  1. 1.
    Alur, R., La Torre, S., Madhusudan, P.: Playing games with boxes and diamonds. In: Amadio, R., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 128–143. Springer, Heidelberg (2003). doi: 10.1007/978-3-540-45187-7_8 CrossRefGoogle Scholar
  2. 2.
    Andersson, D.: An improved algorithm for discounted payoff games. In: ESSLLI Student Session, pp. 91–98 (2006)Google Scholar
  3. 3.
    Beeri, C.: On the membership problem for functional and multivalued dependencies in relational databases. ACM Trans. Database Syst. 5(3), 241–259 (1980)CrossRefzbMATHGoogle Scholar
  4. 4.
    Berthé, V., Rigo, M. (eds.): Combinatorics, Words and Symbolic Dynamics, vol. 135. Cambridge University Press, Cambridge (2016)zbMATHGoogle Scholar
  5. 5.
    Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 140–156. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-02658-4_14 CrossRefGoogle Scholar
  6. 6.
    Boker, U., Henzinger, T.A., Otop, J.: The target discounted-sum problem. In: LICS Proceedings, pp. 750–761. IEEE Computer Society (2015)Google Scholar
  7. 7.
    Bouyer, P., Brenguier, R., Markey, N., Ummels, M.: Pure Nash equilibria in concurrent deterministic games. Logical Methods Comput. Sci. 11(2) (2015)Google Scholar
  8. 8.
    Brenguier, R.: Robust equilibria in mean-payoff games. In: Jacobs, B., Löding, C. (eds.) FoSSaCS 2016. LNCS, vol. 9634, pp. 217–233. Springer, Heidelberg (2016). doi: 10.1007/978-3-662-49630-5_13 CrossRefGoogle Scholar
  9. 9.
    Brenguier, R., Clemente, L., Hunter, P., Pérez, G.A., Randour, M., Raskin, J.-F., Sankur, O., Sassolas, M.: Non-zero sum games for reactive synthesis. In: Dediu, A.-H., Janoušek, J., Martín-Vide, C., Truthe, B. (eds.) LATA 2016. LNCS, vol. 9618, pp. 3–23. Springer, Cham (2016). doi: 10.1007/978-3-319-30000-9_1 CrossRefGoogle Scholar
  10. 10.
    Brenguier, R., Raskin, J.-F., Sankur, O.: Assume-admissible synthesis. Acta Inf. 54(1), 41–83 (2017)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Brihaye, T., Bruyère, V., Meunier, N., Raskin, J-F.: Weak subgame perfect equilibria and their application to quantitative reachability. In: CSL Proceedings. LIPIcs, vol. 41, pp. 504–518. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)Google Scholar
  12. 12.
    Brihaye, T., De Pril, J., Schewe, S.: Multiplayer cost games with simple nash equilibria. In: Artemov, S., Nerode, A. (eds.) LFCS 2013. LNCS, vol. 7734, pp. 59–73. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-35722-0_5 CrossRefGoogle Scholar
  13. 13.
    Bruyère, V., Hautem, Q., Raskin, J-F.: On the complexity of heterogeneous multidimensional games. In: CONCUR Proceedings. LIPIcs, vol. 59, pp. 11:1–11:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)Google Scholar
  14. 14.
    Bruyère, V., Meunier, N., Raskin, J-F.: Secure equilibria in weighted games. In: CSL-LICS Proceedings, pp. 26:1–26:26. ACM (2014)Google Scholar
  15. 15.
    Bruyère, V., Le Roux, S., Pauly, A., Raskin, J.-F.: On the existence of weak subgame perfect equilibria. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 145–161. Springer, Heidelberg (2017). doi: 10.1007/978-3-662-54458-7_9 CrossRefGoogle Scholar
  16. 16.
    Buhrke, N., Lescow, H., Vöge, J.: Strategy construction in infinite games with Streett and Rabin chain winning conditions. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 207–224. Springer, Heidelberg (1996). doi: 10.1007/3-540-61042-1_46 CrossRefGoogle Scholar
  17. 17.
    Calude, C., Jain, S., Khoussainov, B., Li, W., Stephan, F.: Deciding parity games in quasipolynomial time. In: STOC Proceedings. ACM (2017, to appear)Google Scholar
  18. 18.
    Chatterjee, K., Doyen, L., Filiot, E., Raskin, J.-F.: Doomsday equilibria for omega-regular games. Inf. Comput. 254, 296–315 (2017)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. ACM Trans. Comput. Logic 11, 23 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Chatterjee, K., Doyen, L., Randour, M., Raskin, J.-F.: Looking at mean-payoff and total-payoff through windows. Inf. Comput. 242, 25–52 (2015)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Chatterjee, K., Dvorák, W., Henzinger, M., Loitzenbauer, V.: Conditionally optimal algorithms for generalized Büchi games. In: MFCS Proceedings. LIPIcs, vol. 58, pp. 25:1–25:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)Google Scholar
  22. 22.
    Chatterjee, K., Henzinger, M.: Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition. J. ACM 61(3), 15:1–15:40 (2014)CrossRefzbMATHGoogle Scholar
  23. 23.
    Chatterjee, K., Henzinger, T.A., Jurdzinski, M.: Games with secure equilibria. Theor. Comput. Sci. 365, 67–82 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Chatterjee, K., Henzinger, T.A., Piterman, N.: Generalized parity games. In: Seidl, H. (ed.) FoSSaCS 2007. LNCS, vol. 4423, pp. 153–167. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-71389-0_12 CrossRefGoogle Scholar
  25. 25.
    Chatterjee, K., Majumdar, R., Jurdziński, M.: On nash equilibria in stochastic games. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 26–40. Springer, Heidelberg (2004). doi: 10.1007/978-3-540-30124-0_6 CrossRefGoogle Scholar
  26. 26.
    Condurache, R., Filiot, E., Gentilini, R., Raskin, J-F.: The complexity of rational synthesis. In: Proceedings of ICALP. LIPIcs, vol. 55, pp. 121:1–121:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)Google Scholar
  27. 27.
    De Pril, J.: Equilibria in Multiplayer Cost Games. Ph. D. thesis, University UMONS (2013)Google Scholar
  28. 28.
    De Pril, J., Flesch, J., Kuipers, J., Schoenmakers, G., Vrieze, K.: Existence of secure equilibrium in multi-player games with perfect information. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014. LNCS, vol. 8635, pp. 213–225. Springer, Heidelberg (2014). doi: 10.1007/978-3-662-44465-8_19 Google Scholar
  29. 29.
    Emerson, E.A.: Automata, tableaux, and temporal logics (extended abstract). In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 79–88. Springer, Heidelberg (1985). doi: 10.1007/3-540-15648-8_7 CrossRefGoogle Scholar
  30. 30.
    Emerson, E.A., Jutla, C.S.: Tree automata, Mu-calculus and determinacy. In: FOCS Proceedings, pp. 368–377. IEEE Computer Society (1991)Google Scholar
  31. 31.
    Emerson, E.A., Lei, C.-L.: Modalities for model checking: branching time logic strikes back. Sci. Comput. Program. 8(3), 275–306 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  32. 32.
    Fijalkow, N., Horn, F.: Les jeux d’accessibilité généralisée. Tech. Sci. Informatiques 32(9–10), 931–949 (2013)CrossRefGoogle Scholar
  33. 33.
    Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, New York (1997)zbMATHGoogle Scholar
  34. 34.
    Flesch, J., Kuipers, J., Mashiah-Yaakovi, A., Schoenmakers, G., Solan, E., Vrieze, K.: Perfect-information games with lower-semicontinuous payoffs. Math. Oper. Res. 35, 742–755 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  35. 35.
    Fudenberg, D., Levine, D.: Subgame-perfect equilibria of finite-and infinite-horizon games. J. Econ. Theor. 31, 251–268 (1983)MathSciNetCrossRefzbMATHGoogle Scholar
  36. 36.
    Gimbert, H., Zielonka, W.: When can you play positionally? In: Fiala, J., Koubek, V., Kratochvíl, J. (eds.) MFCS 2004. LNCS, vol. 3153, pp. 686–697. Springer, Heidelberg (2004). doi: 10.1007/978-3-540-28629-5_53 CrossRefGoogle Scholar
  37. 37.
    Gimbert, H., Zielonka, W.: Games where you can play optimally without any memory. In: Abadi, M., Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 428–442. Springer, Heidelberg (2005). doi: 10.1007/11539452_33 CrossRefGoogle Scholar
  38. 38.
    Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games: A Guide to Current Research. LNCS, vol. 2500. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  39. 39.
    Grädel, E., Ummels, M.: Solution concepts and algorithms for infinite multiplayer games. In: Apt, K., van Rooij, R. (eds.) New Perspectives on Games and Interaction, vol. 4, pp. 151–178. Amsterdam University Press, Amsterdam (2008)Google Scholar
  40. 40.
    Harris, C.: Existence and characterization of perfect equilibrium in games of perfect information. Econometrica 53, 613–628 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  41. 41.
    Horn, F.: Explicit muller games are PTIME. In: FSTTCS Proceedings. LIPIcs, vol. 2, pp. 235–243. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2008)Google Scholar
  42. 42.
    Hunter, P., Dawar, A.: Complexity bounds for regular games. In: Jȩdrzejowicz, J., Szepietowski, A. (eds.) MFCS 2005. LNCS, vol. 3618, pp. 495–506. Springer, Heidelberg (2005). doi: 10.1007/11549345_43 CrossRefGoogle Scholar
  43. 43.
    Hunter, P., Raskin, J-F.: Quantitative games with interval objectives. In: FSTTCS Proceedings. LIPIcs, vol. 29, pp. 365–377. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2014)Google Scholar
  44. 44.
    Immerman, N.: Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sci. 22, 384–406 (1981)MathSciNetCrossRefzbMATHGoogle Scholar
  45. 45.
    Jones, N.D.: Space-bounded reducibility among combinatorial problems. J. Comput. Syst. Sci. 11, 68–75 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  46. 46.
    Jurdzinski, M.: Deciding the winner in parity games is in UP \(\cap \) co-UP. Inf. Process. Lett. 68(3), 119–124 (1998)MathSciNetCrossRefzbMATHGoogle Scholar
  47. 47.
    Karp, R.M.: A characterization of the minimum cycle mean in a digraph. Discrete Math. 23, 309–311 (1978)MathSciNetCrossRefzbMATHGoogle Scholar
  48. 48.
    Kopczyński, E.: Half-positional determinacy of infinite games. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 336–347. Springer, Heidelberg (2006). doi: 10.1007/11787006_29 CrossRefGoogle Scholar
  49. 49.
    Kuhn, H.W.: Extensive games and the problem of information. In: Classics in Game Theory, pp. 46–68 (1953)Google Scholar
  50. 50.
    Lothaire, M.: Algebraic Combinatorics on Words, vol. 90. Cambridge University Press, Cambridge (2002)CrossRefzbMATHGoogle Scholar
  51. 51.
    Martin, D.A.: Borel determinacy. Ann. Math. 102, 363–371 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  52. 52.
    McNaughton, R.: Infinite games played on finite graphs. Ann. Pure Appl. Logic 65(2), 149–184 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  53. 53.
    Nash, J.F.: Equilibrium points in \(n\)-person games. In: PNAS, vol. 36, pp. 48–49. National Academy of Sciences (1950)Google Scholar
  54. 54.
    Osborne, M.J., Rubinstein, A.: A Course in Game Theory. MIT Press, Cambridge (1994)zbMATHGoogle Scholar
  55. 55.
    Perrin, D., Pin, J.-E.: Infinite Words, Automata, Semigroups, Logic and Games, vol. 141. Elsevier, Amsterdam (2004)zbMATHGoogle Scholar
  56. 56.
    Piterman, N., Pnueli, A.: Faster solutions of Rabin and Streett games. In: LICS Proceedings, pp. 275–284. IEEE Computer Society (2006)Google Scholar
  57. 57.
    Purves, R.A., Sudderth, W.D.: Perfect information games with upper semicontinuous payoffs. Math. Oper. Res. 36(3), 468–473 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  58. 58.
    Rényi, A.: Representations of real numbers and their ergodic properties. Acta Math. Acad. Scientiarum Hung. 8(3–4), 477–493 (1957)MathSciNetCrossRefzbMATHGoogle Scholar
  59. 59.
    Le Roux, S., Pauly, A.: Extending finite memory determinacy to multiplayer games. In: Proceedings of SR. EPTCS, vol. 218, pp. 27–40 (2016)Google Scholar
  60. 60.
    Safra, S., Vardi, M.Y.: On omega-automata and temporal logic (preliminary report). In: Proceedings of STOC, pp. 127–137. ACM (1989)Google Scholar
  61. 61.
    Selten, R.: Spieltheoretische Behandlung eines Oligopolmodells mit Nachfrageträgheit. Z. die gesamte Staatswissenschaft 121, 301–324 (1965). pp. 667–689Google Scholar
  62. 62.
    Solan, E., Vieille, N.: Deterministic multi-player Dynkin games. J. Math. Econ. 39, 911–929 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  63. 63.
    Ummels, M.: Rational behaviour and strategy construction in infinite multiplayer games. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 212–223. Springer, Heidelberg (2006). doi: 10.1007/11944836_21 CrossRefGoogle Scholar
  64. 64.
    Ummels, M.: The complexity of nash equilibria in infinite multiplayer games. In: Amadio, R. (ed.) FoSSaCS 2008. LNCS, vol. 4962, pp. 20–34. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-78499-9_3 CrossRefGoogle Scholar
  65. 65.
    Ummels, M., Wojtczak, D.: The complexity of nash equilibria in limit-average games. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 482–496. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-23217-6_32 CrossRefGoogle Scholar
  66. 66.
    Ummels, M., Wojtczak, D.: The complexity of Nash equilibria in limit-average games. CoRR, abs/1109.6220 (2011)Google Scholar
  67. 67.
    Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  68. 68.
    Velner, Y.: Robust multidimensional mean-payoff games are undecidable. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol. 9034, pp. 312–327. Springer, Heidelberg (2015). doi: 10.1007/978-3-662-46678-0_20 CrossRefGoogle Scholar
  69. 69.
    Velner, Y., Chatterjee, K., Doyen, L., Henzinger, T.A., Rabinovich, A.M., Raskin, J.-F.: The complexity of multi-mean-payoff and multi-energy games. Inf. Comput. 241, 177–196 (2015)MathSciNetCrossRefzbMATHGoogle Scholar
  70. 70.
    von Neumann, J., Morgenstern, O.: Theory of Games and Economic Behavior. Princeton University Press, Princeton (1944)zbMATHGoogle Scholar
  71. 71.
    Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theor. Comput. Sci. 158, 343–359 (1996)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Computer Science DepartmentUniversity of MonsMonsBelgium

Personalised recommendations