Top

Published in:

2017 | OriginalPaper | Chapter

Computer Aided Synthesis: A Game-Theoretic Approach

Author : Véronique Bruyère

Published in: Developments in Language Theory

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

next chapter A Comprehensive Introduction to the Theory of Word-Representable Graphs

Available only for authorised users

This condition guarantees that there is no deadlock. It can be assumed w.l.o.g. for all the problems considered in this article.

We also say that player i controls the vertices of \(V_i\).

that is, an irreflexive, transitive and total binary relation.

In all examples of this article, circle (resp. square) vertices are controlled by player 1 (resp. player 2).

This informal definition is enough for this survey. See for instance [38] for a definition.

As player 1 can only loop on vertices \(v_2\) and \(v_3\), we do not formally define \(\sigma _1\) on histories ending with \(v_2\) or \(v_3\).

This problem is focused on Player 1, the payoff function \(f_2\) and preference relation \(\prec _2\) of Player 2 do not matter.

Alternatively, \(\prec _i\) can be the ordering > meaning that player i prefers to minimize the payoff of a play.

A colored variant of Muller objective is defined from a coloring \(c~: V \rightarrow \mathbb N\) of the vertices: the family \(\mathcal F\) is composed of subsets of \(c(V)\) (instead of V) and \(\varOmega _i = \{\rho \in Plays\mid inf(c(\rho _0)c(\rho _1)\ldots ) \in \mathcal{F} \}\) [39]. See [42] for several variants of Muller games.

In Sect. 3.1, we omit index 1 everywhere since player 1 is the unique player of the game.

The hypotheses of this theorem are those given in the full version of [36] available at http://www.labri.fr/perso/gimbert/.

Theorem 20 is given in [36] for real-valued payoff functions \(f : Plays\rightarrow \mathbb R\) and the usual ordering <, but its proof is easily generalized to the statement given here.

It is PSPACE-complete for the colored variant of Muller objective [42, 52].

The reader who prefers to know classical solutions to Problem 7 for multi-player non zero-sum games can skip this section and go directly to Sect. 4.

This tuple of payoff functions is used by player 1 contrarily to Definition 2 where function \(f_i\) is used by player i for all \(i \in \varPi \).

We found no reference for this result. The PSPACE membership (resp. the finite memory of the strategies) follows from [1] (resp. [13]). In [1], games with a union of a Streett objective and a Rabin objective are shown to be PSPACE-hard. It is thus also the case for games with a union of Streett objectives. By Martin’s theorem, it follows that games with an intersection of Rabin objectives are PSPACE-hard.

Recall that the payoff function and the preference relation of the second player do not matter in two-player zero-sum games.

In [12], one hypothesis is missing: the required optimal strategies must be uniform.

We found no reference for Muller objectives. A sketch of proof is given in the appendix. Problem 7 is PSPACE-complete for the colored variant of Muller objectives [26].

Recall our comment after Theorem 22.

The reduction is given for another kind of solution profile but it also works for NEs.

The definition was given for player 1.

A restriction to two-player games is necessary to deal with a secure preference that is total.

In this particular context, plays are finite paths.

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 CrossRef

Andersson, D.: An improved algorithm for discounted payoff games. In: ESSLLI Student Session, pp. 91–98 (2006)

Beeri, C.: On the membership problem for functional and multivalued dependencies in relational databases. ACM Trans. Database Syst. 5(3), 241–259 (1980)CrossRefMATH

Berthé, V., Rigo, M. (eds.): Combinatorics, Words and Symbolic Dynamics, vol. 135. Cambridge University Press, Cambridge (2016)MATH

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 CrossRef

Boker, U., Henzinger, T.A., Otop, J.: The target discounted-sum problem. In: LICS Proceedings, pp. 750–761. IEEE Computer Society (2015)

Bouyer, P., Brenguier, R., Markey, N., Ummels, M.: Pure Nash equilibria in concurrent deterministic games. Logical Methods Comput. Sci. 11(2) (2015)

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 CrossRef

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 CrossRef

10.

Brenguier, R., Raskin, J.-F., Sankur, O.: Assume-admissible synthesis. Acta Inf. 54(1), 41–83 (2017)MathSciNetCrossRefMATH

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)

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 CrossRef

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)

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)

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 CrossRef

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 CrossRef

17.

Calude, C., Jain, S., Khoussainov, B., Li, W., Stephan, F.: Deciding parity games in quasipolynomial time. In: STOC Proceedings. ACM (2017, to appear)

18.

Chatterjee, K., Doyen, L., Filiot, E., Raskin, J.-F.: Doomsday equilibria for omega-regular games. Inf. Comput. 254, 296–315 (2017)MathSciNetCrossRefMATH

19.

Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. ACM Trans. Comput. Logic 11, 23 (2010)MathSciNetCrossRefMATH

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)MathSciNetCrossRefMATH

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)

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)CrossRefMATH

23.

Chatterjee, K., Henzinger, T.A., Jurdzinski, M.: Games with secure equilibria. Theor. Comput. Sci. 365, 67–82 (2006)MathSciNetCrossRefMATH

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 CrossRef

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 CrossRef

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)

27.

De Pril, J.: Equilibria in Multiplayer Cost Games. Ph. D. thesis, University UMONS (2013)

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

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 CrossRef

30.

Emerson, E.A., Jutla, C.S.: Tree automata, Mu-calculus and determinacy. In: FOCS Proceedings, pp. 368–377. IEEE Computer Society (1991)

31.

Emerson, E.A., Lei, C.-L.: Modalities for model checking: branching time logic strikes back. Sci. Comput. Program. 8(3), 275–306 (1987)MathSciNetCrossRefMATH

32.

Fijalkow, N., Horn, F.: Les jeux d’accessibilité généralisée. Tech. Sci. Informatiques 32(9–10), 931–949 (2013)CrossRef

33.

Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, New York (1997)MATH

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)MathSciNetCrossRefMATH

35.

Fudenberg, D., Levine, D.: Subgame-perfect equilibria of finite-and infinite-horizon games. J. Econ. Theor. 31, 251–268 (1983)MathSciNetCrossRefMATH

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 CrossRef

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 CrossRef

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)MATH

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)

40.

Harris, C.: Existence and characterization of perfect equilibrium in games of perfect information. Econometrica 53, 613–628 (1985)MathSciNetCrossRefMATH

41.

Horn, F.: Explicit muller games are PTIME. In: FSTTCS Proceedings. LIPIcs, vol. 2, pp. 235–243. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2008)

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 CrossRef

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)

44.

Immerman, N.: Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sci. 22, 384–406 (1981)MathSciNetCrossRefMATH

45.

Jones, N.D.: Space-bounded reducibility among combinatorial problems. J. Comput. Syst. Sci. 11, 68–75 (1975)MathSciNetCrossRefMATH

46.

Jurdzinski, M.: Deciding the winner in parity games is in UP \(\cap \) co-UP. Inf. Process. Lett. 68(3), 119–124 (1998)MathSciNetCrossRefMATH

47.

Karp, R.M.: A characterization of the minimum cycle mean in a digraph. Discrete Math. 23, 309–311 (1978)MathSciNetCrossRefMATH

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 CrossRef

49.

Kuhn, H.W.: Extensive games and the problem of information. In: Classics in Game Theory, pp. 46–68 (1953)

50.

Lothaire, M.: Algebraic Combinatorics on Words, vol. 90. Cambridge University Press, Cambridge (2002)CrossRefMATH

51.

Martin, D.A.: Borel determinacy. Ann. Math. 102, 363–371 (1975)MathSciNetCrossRefMATH

52.

McNaughton, R.: Infinite games played on finite graphs. Ann. Pure Appl. Logic 65(2), 149–184 (1993)MathSciNetCrossRefMATH

53.

Nash, J.F.: Equilibrium points in \(n\)-person games. In: PNAS, vol. 36, pp. 48–49. National Academy of Sciences (1950)

54.

Osborne, M.J., Rubinstein, A.: A Course in Game Theory. MIT Press, Cambridge (1994)MATH

55.

Perrin, D., Pin, J.-E.: Infinite Words, Automata, Semigroups, Logic and Games, vol. 141. Elsevier, Amsterdam (2004)MATH

56.

Piterman, N., Pnueli, A.: Faster solutions of Rabin and Streett games. In: LICS Proceedings, pp. 275–284. IEEE Computer Society (2006)

57.

Purves, R.A., Sudderth, W.D.: Perfect information games with upper semicontinuous payoffs. Math. Oper. Res. 36(3), 468–473 (2011)MathSciNetCrossRefMATH

58.

Rényi, A.: Representations of real numbers and their ergodic properties. Acta Math. Acad. Scientiarum Hung. 8(3–4), 477–493 (1957)MathSciNetCrossRefMATH

59.

Le Roux, S., Pauly, A.: Extending finite memory determinacy to multiplayer games. In: Proceedings of SR. EPTCS, vol. 218, pp. 27–40 (2016)

60.

Safra, S., Vardi, M.Y.: On omega-automata and temporal logic (preliminary report). In: Proceedings of STOC, pp. 127–137. ACM (1989)

61.

Selten, R.: Spieltheoretische Behandlung eines Oligopolmodells mit Nachfrageträgheit. Z. die gesamte Staatswissenschaft 121, 301–324 (1965). pp. 667–689

62.

Solan, E., Vieille, N.: Deterministic multi-player Dynkin games. J. Math. Econ. 39, 911–929 (2003)MathSciNetCrossRefMATH

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 CrossRef

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 CrossRef

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 CrossRef

66.

Ummels, M., Wojtczak, D.: The complexity of Nash equilibria in limit-average games. CoRR, abs/1109.6220 (2011)

67.

Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994)MathSciNetCrossRefMATH

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 CrossRef

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)MathSciNetCrossRefMATH

70.

von Neumann, J., Morgenstern, O.: Theory of Games and Economic Behavior. Princeton University Press, Princeton (1944)MATH

71.

Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theor. Comput. Sci. 158, 343–359 (1996)MathSciNetCrossRefMATH

Title: Computer Aided Synthesis: A Game-Theoretic Approach
Author: Véronique Bruyère
Publisher: Springer International Publishing
Book: Developments in Language Theory
Print ISBN: 978-3-319-62808-0

Electronic ISBN: 978-3-319-62809-7

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-319-62809-7_1

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner