Skip to main content
SpringerLink
Log in

Doomsday Equilibria for Omega-Regular Games

  • Conference paper
Verification, Model Checking, and Abstract Interpretation (VMCAI 2014)

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

Abstract

Two-player games on graphs provide the theoretical framework for many important problems such as reactive synthesis. While the traditional study of two-player zero-sum games has been extended to multi-player games with several notions of equilibria, they are decidable only for perfect-information games, whereas several applications require imperfect-information games.

In this paper we propose a new notion of equilibria, called doomsday equilibria, which is a strategy profile such that all players satisfy their own objective, and if any coalition of players deviates and violates even one of the players objective, then the objective of every player is violated.

We present algorithms and complexity results for deciding the existence of doomsday equilibria for various classes of ω-regular objectives, both for imperfect-information games, and for perfect-information games.We provide optimal complexity bounds for imperfect-information games, and in most cases for perfect-information games.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM 49, 672–713 (2002)

    Article  MathSciNet  Google Scholar 

  2. Alur, R., La Torre, S.: Deterministic generators and games for LTL fragments. TOCL 5 (2004)

    Google Scholar 

  3. Alur, R., La Torre, S., Madhusudan, P.: Playing games with boxes and diamonds. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 128–143. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  4. Berwanger, D., Doyen, L.: On the power of imperfect information. In: FSTTCS, pp. 73–82 (2008)

    Google Scholar 

  5. Büchi, J.R., Landweber, L.H.: Definability in the monadic second-order theory of successor. J. Symb. Log. 34(2), 166–170 (1969)

    Article  MATH  Google Scholar 

  6. Cai, Y., Zhang, T., Luo, H.: An improved lower bound for the complementation of rabin automata. In: LICS, pp. 167–176. IEEE Computer Society (2009)

    Google Scholar 

  7. Chadha, R., Kremer, S., Scedrov, A.: Formal analysis of multiparty contract signing. J. Autom. Reasoning 36(1-2), 39–83 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  8. Chatterjee, K., Doyen, L., Filiot, E., Raskin, J.-F.: Doomsday equilibria for omega-regular games. CoRR, abs/1311.3238 (2013)

    Google Scholar 

  9. Chatterjee, K., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Algorithms for omega-regular games with imperfect information. LMCS 3(3) (2007)

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

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

    Chapter  Google Scholar 

  13. Da Costa Lopes, A., Laroussinie, F., Markey, N.: ATL with strategy contexts: Expressiveness and model checking. In: FSTTCS. LIPIcs, vol. 8, pp. 120–132 (2010)

    Google Scholar 

  14. Emerson, E.A., Jutla, C.: Tree automata, mu-calculus and determinacy. In: FOCS, pp. 368–377. IEEE Comp. Soc. (1991)

    Google Scholar 

  15. Emerson, E.A., Lei, C.-L.: Modalities for model checking: Branching time strikes back. In: POPL, pp. 84–96 (1985)

    Google Scholar 

  16. 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 

  17. Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games, vol. 2500. Springer (2002)

    Google Scholar 

  18. Immerman, N.: Number of quantifiers is better than number of tape cells. Journal of Computer and System Sciences 22, 384–406 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  19. Jamroga, W., Mauw, S., Melissen, M.: Fairness in non-repudiation protocols. In: Meadows, C., Fernandez-Gago, C. (eds.) STM 2011. LNCS, vol. 7170, pp. 122–139. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  20. Kremer, S., Raskin, J.-F.: A game-based verification of non-repudiation and fair exchange protocols. Journal of Computer Security 11(3), 399–430 (2003)

    Google Scholar 

  21. Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: FOCS (2005)

    Google Scholar 

  22. Martin, D.: Borel determinacy. Annals of Mathematics 102, 363–371 (1975)

    Article  MATH  MathSciNet  Google Scholar 

  23. Mogavero, F., Murano, A., Perelli, G., Vardi, M.Y.: What makes Atl* decidable? A decidable fragment of strategy logic. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 193–208. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

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

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  26. Piterman, N.: From nondeterministic Büchi and streett automata to deterministic parity automata. Logical Methods in Computer Science 3(3) (2007)

    Google Scholar 

  27. Piterman, N., Pnueli, A.: Faster solutions of rabin and streett games. In: LICS, pp. 275–284 (2006)

    Google Scholar 

  28. Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179–190. ACM Press (1989)

    Google Scholar 

  29. Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc. 141, 1–35 (1969)

    MATH  MathSciNet  Google Scholar 

  30. Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete event processes. SIAM Journal on Control and Optimization 25(1), 206–230 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  31. Shapley, L.S.: Stochastic games. PNAS 39, 1095–1100 (1953)

    Article  MATH  MathSciNet  Google Scholar 

  32. Ummels, M., Wojtczak, D.: The complexity of nash equilibria in stochastic multiplayer games. Logical Methods in Computer Science 7(3) (2011)

    Google Scholar 

  33. Wang, F., Huang, C.-H., Yu, F.: A temporal logic for the interaction of strategies. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 466–481. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IST Austria, Austria

    Krishnendu Chatterjee

  2. LSV, ENS Cachan & CNRS, France

    Laurent Doyen

  3. CS, Université Libre de Bruxelles – U.L.B, Belgium

    Emmanuel Filiot & Jean-François Raskin

Authors
  1. Krishnendu Chatterjee
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Laurent Doyen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Emmanuel Filiot
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jean-François Raskin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. One Microsoft Way, Microsoft Research, 98052, Redmond, WA, USA

    Kenneth L. McMillan

  2. DI - Ecole Normale Supérieure, 45, rue d’Ulm, 75230, Paris Cedex 05, France

    Xavier Rival

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Chatterjee, K., Doyen, L., Filiot, E., Raskin, JF. (2014). Doomsday Equilibria for Omega-Regular Games. In: McMillan, K.L., Rival, X. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2014. Lecture Notes in Computer Science, vol 8318. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54013-4_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-54013-4_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-54012-7

  • Online ISBN: 978-3-642-54013-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation