Skip to main content
SpringerLink
Log in

Non-Zero Sum Games for Reactive Synthesis

  • Conference paper
  • First Online:
Language and Automata Theory and Applications (LATA 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9618))

Included in the following conference series:

Abstract

In this invited contribution, we summarize new solution concepts useful for the synthesis of reactive systems that we have introduced in several recent publications. These solution concepts are developed in the context of non-zero sum games played on graphs. They are part of the contributions obtained in the inVEST project funded by the European Research Council.

Work supported by the ERC starting grant inVEST (FP7-279499), G.A. Pérez is supported by F.R.S.-FNRS ASP fellowship, M. Randour is a F.R.S.-FNRS Postdoctoral Researcher.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    To define word strategies, it is convenient to consider game arenas where edges have labels called letters. In that case, when playing a word strategy, Adam commits to a sequence of letters (i.e., a word) and plays that word regardless of the exact state of the game. Word strategies are formally defined in [32] and below.

  2. 2.

    It should be noted that we can easily consider finite-memory randomized strategies for Adam, instead of memoryless randomized strategies. This is because we can always take the synchronized product of a finite-memory randomized strategy with the game arena to obtain a new game arena in which the finite-memory strategy on the original game arena is now equivalent to a memoryless strategy.

References

  1. Aminof, B., Kupferman, O., Lampert, R.: Reasoning about online algorithms with weighted automata. ACM Trans. Algorithms 6(2), 28:1–28:36 (2010). doi:10.1145/1721837.1721844. http://doi.acm.org/10.1145/1721837.1721844

    Article  MathSciNet  Google Scholar 

  2. Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  3. Berwanger, D.: Admissibility in infinite games. In: Thomas, W., Weil, P. (eds.) STACS 2007. LNCS, vol. 4393, pp. 188–199. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  4. Bloem, R., Ehlers, R., Jacobs, S., Könighofer, R.: How to handle assumptions in synthesis. In: Proceedings of SYNT. EPTCS, vol. 157, pp. 34–50 (2014)

    Google Scholar 

  5. Brandenburger, A., Friedenberg, A., Keisler, H.J.: Admissibility in games. Econometrica 76(2), 307–352 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  6. Brázdil, T., Chatterjee, K., Forejt, V., Kucera, A.: Trading performance for stability in Markov decision processes. In: Proceedings of LICS, pp. 331–340. IEEE (2013)

    Google Scholar 

  7. Brenguier, R., Raskin, J.-F., Sankur, O.: Assume-admissible synthesis. In: Proceedings of CONCUR. LIPIcs, vol. 42, pp. 100–113. Schloss Dagstuhl-LZI (2015)

    Google Scholar 

  8. Brenguier, R., Raskin, J.-F., Sassolas, M.: The complexity of admissibility in omega-regular games. In: Proceedings of CSL-LICS, pp. 23:1–23:10. ACM (2014)

    Google Scholar 

  9. Brihaye, T., Bruyère, V., Meunier, N., Raskin, J.-F.: Weak subgame perfect equilibria and their application to quantitative reachability. In: Proceedings of CSL. LIPIcs, vol. 41, pp. 504–518. Schloss Dagstuhl - LZI (2015)

    Google Scholar 

  10. Brim, L., Chaloupka, J., Doyen, L., Gentilini, R., Raskin, J.-F.: Faster algorithms for mean-payoff games. Formal Methods Syst. Des. 38(2), 97–118 (2011)

    Article  MATH  Google Scholar 

  11. Bruyère, V., Filiot, E., Randour, M., Raskin, J.-F.: Expectations or guarantees? I want it all! A crossroad between games and MDPs. In: Proceedings of SR. EPTCS, vol. 146, pp. 1–8 (2014)

    Google Scholar 

  12. Bruyère, V., Filiot, E., Randour, M., Raskin, J.-F.: Meet your expectations with guarantees: beyond worst-case synthesis in quantitative games. In: Proceedings of STACS. LIPIcs, vol. 25, pp. 199–213. Schloss Dagstuhl - LZI (2014)

    Google Scholar 

  13. Bruyère, V., Meunier, N., Raskin, J.-F.: Secure equilibria in weighted games. In: Proceedings of CSL-LICS, pp. 26:1–26:26. ACM (2014)

    Google Scholar 

  14. Chatterjee, K., Doyen, L., Filiot, E., Raskin, J.-F.: Doomsday equilibria for omega-regular games. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 78–97. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  15. Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. ACM Trans. Comput. Logic 11(4), 23:1–23:38 (2010). doi:10.1145/1805950.1805953. http://doi.acm.org/10.1145/1805950.1805953

    MathSciNet  Google Scholar 

  16. Chatterjee, K., Doyen, L., Randour, M., Raskin, J.-F.: Looking at mean-payoff and total-payoff through windows. Inf. Comput. 242, 25–52 (2015)

    Article  MathSciNet  Google Scholar 

  17. Chatterjee, K., Henzinger, T.A.: Assume-guarantee synthesis. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 261–275. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  18. Chatterjee, K., Henzinger, T.A., Jurdziński, M.: Games with secure equilibria. Theoret. Comput. Sci. 365(1), 67–82 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  19. Chatterjee, K., Henzinger, T.A., Piterman, N.: Strategy logic. Inf. Comput. 208(6), 677–693 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  20. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logics of Programs. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1981)

    Chapter  Google Scholar 

  21. Clemente, L., Raskin, J.-F.: Multidimensional beyond worst-case and almost-sure problems for mean-payoff objectives. In: Proceedings of LICS, pp. 257–268. IEEE (2015)

    Google Scholar 

  22. Colcombet, T.: Forms of determinism for automata. In: Proceedings of STACS. LIPIcs, vol. 14, pp. 1–23. Schloss Dagstuhl - LZI (2012)

    Google Scholar 

  23. Damm, W., Finkbeiner, B.: Does it pay to extend the perimeter of a world model? In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 12–26. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  24. Ehrenfeucht, A., Mycielski, J.: Positional strategies for mean payoff games. Int. J. Game Theory 8, 109–113 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  25. Faella, M.: Admissible strategies in infinite games over graphs. In: Královič, R., Niwiński, D. (eds.) MFCS 2009. LNCS, vol. 5734, pp. 307–318. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  26. Filar, J., Vrieze, K.: Competitive Markov decision processes. Springer, New York (1997)

    MATH  Google Scholar 

  27. Filar, J.A., Krass, D., Ross, K.W.: Percentile performance criteria for limiting average Markov decision processes. Trans. Autom. Control 40, 2–10 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  28. Filiot, E., Le Gall, T., Raskin, J.-F.: Iterated regret minimization in game graphs. In: Hliněný, P., Kučera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 342–354. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  29. Fisman, D., Kupferman, O., Lustig, Y.: Rational synthesis. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 190–204. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  30. Halpern, J.Y., Pass, R.: Iterated regret minimization: a new solution concept. Games Econ. Behav. 74(1), 184–207 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  31. Henzinger, T.A., Piterman, N.: Solving games without determinization. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 395–410. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  32. Hunter, P., Pérez, G.A., Raskin, J.-F.: Reactive synthesis without regret. In: Proceedings of CONCUR. LIPIcs, vol. 42, pp. 114–127. Schloss Dagstuhl - LZI (2015)

    Google Scholar 

  33. Khachiyan, L., Boros, E., Borys, K., Elbassioni, K., Gurvich, V., Rudolf, G., Zhao, J.: On short paths interdiction problems: total and node-wise limited interdiction. Theory Comput. Syst. 43, 204–233 (2008)

    Article  MathSciNet  Google Scholar 

  34. Kupferman, O., Perelli, G., Vardi, M.Y.: Synthesis with rational environments. In: Bulling, N. (ed.) EUMAS 2014. LNCS, vol. 8953, pp. 219–235. Springer, Heidelberg (2015)

    Google Scholar 

  35. Mannor, S., Tsitsiklis, J.: Mean-variance optimization in Markov decision processes. In: Proceedings of ICML, pp. 177–184. Omnipress (2011)

    Google Scholar 

  36. Mogavero, F., Murano, A., Vardi, M.Y.: Reasoning about strategies. In: Proceedings of FSTTCS, LIPIcs, vol. 8, pp. 133–144. Schloss Dagstuhl - LZI (2010)

    Google Scholar 

  37. Nash, J.: Equilibrium points in \(n\)-person games. PNAS 36, 48–49 (1950)

    Article  MathSciNet  MATH  Google Scholar 

  38. Puterman, M.: Markov decision processes: discrete stochastic dynamic programming, 1st edn. Wiley, New York (1994)

    Book  MATH  Google Scholar 

  39. Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) International Symposium on Programming. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982)

    Chapter  Google Scholar 

  40. Randour, M., Raskin, J.-F., Sankur, O.: Percentile queries in multi-dimensional Markov decision processes. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 123–139. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  41. Randour, M., Raskin, J.-F., Sankur, O.: Variations on the stochastic shortest path problem. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 1–18. Springer, Heidelberg (2015)

    Google Scholar 

  42. 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)

    Chapter  Google Scholar 

  43. Vardi, M.Y.: Automatic verification of probabilistic concurrent finite state programs. In: Proceedings of FOCS, pp. 327–338. IEEE (1985)

    Google Scholar 

  44. Wu, C., Lin, Y.: Minimizing risk models in Markov decision processes with policies depending on target values. J. Math. Anal. Appl. 231(1), 47–67 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  45. Zinkevich, M., Johanson, M., Bowling, M., Piccione, C.: Regret minimization in games with incomplete information. In: Proceedings of NIPS, pp. 905–912 (2008)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Oxford, Oxford, UK

    Romain Brenguier

  2. University of Warsaw, Warsaw, Poland

    Lorenzo Clemente

  3. Université Libre de Bruxelles, Brussels, Belgium

    Paul Hunter, Guillermo A. Pérez, Mickael Randour & Jean-François Raskin

  4. CNRS, IRISA, Rennes, France

    Ocan Sankur

  5. Université Paris-Est – Créteil, LACL, Créteil, France

    Mathieu Sassolas

Authors
  1. Romain Brenguier
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lorenzo Clemente
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Paul Hunter
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Guillermo A. Pérez
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Mickael Randour
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Jean-François Raskin
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Ocan Sankur
    View author publications

    You can also search for this author in PubMed Google Scholar

  8. Mathieu Sassolas
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jean-François Raskin .

Editor information

Editors and Affiliations

  1. Rovira i Virgili University, Tarragona, Spain

    Adrian-Horia Dediu

  2. Czech Technical University, Prague, Czech Republic

    Jan Janoušek

  3. Rovira i Virgili University, Tarragona, Spain

    Carlos Martín-Vide

  4. Justus Liebig University Giessen, Gießen, Germany

    Bianca Truthe

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Brenguier, R. et al. (2016). Non-Zero Sum Games for Reactive Synthesis. In: Dediu, AH., Janoušek, J., Martín-Vide, C., Truthe, B. (eds) Language and Automata Theory and Applications. LATA 2016. Lecture Notes in Computer Science(), vol 9618. Springer, Cham. https://doi.org/10.1007/978-3-319-30000-9_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-30000-9_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-29999-0

  • Online ISBN: 978-3-319-30000-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation