×

zbMATH — the first resource for mathematics

Doomsday equilibria for omega-regular games. (English) Zbl 1370.68164
Summary: 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.
In this paper we propose a new notion of equilibria, called doomsday equilibria, which is a strategy profile where 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 \(\omega\)-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.
MSC:
68Q45 Formal languages and automata
91A43 Games involving graphs
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Althoff, C. Schulte; Thomas, W.; Wallmeier, N., Observations on determinization of Büchi automata, Theor. Comput. Sci., 363, 2, 224-233, (2006) · Zbl 1153.68399
[2] Alur, R.; Henzinger, T. A.; Kupferman, O., Alternating-time temporal logic, J. ACM, 49, 672-713, (2002) · Zbl 1326.68181
[3] Alur, R.; La Torre, S., Deterministic generators and games for LTL fragments, ACM Trans. Comput. Log., 5, (2004) · Zbl 1366.03181
[4] Alur, R.; La Torre, S.; Madhusudan, P., Playing games with boxes and diamonds, (CONCUR, LNCS, vol. 2761, (2003), Springer), 127-141 · Zbl 1274.68173
[5] Baier, Christel; Katoen, Joost-Pieter, Principles of model checking, Representation and Mind Series, (2008), The MIT Press · Zbl 1179.68076
[6] Berwanger, D.; Doyen, L., On the power of imperfect information, (FSTTCS, (2008)), 73-82 · Zbl 1248.68233
[7] Büchi, J. R.; Landweber, L. H., Definability in the monadic second-order theory of successor, J. Symb. Log., 34, 2, 166-170, (1969) · Zbl 0209.02203
[8] Cai, Y.; Zhang, T.; Luo, H., An improved lower bound for the complementation of rabin automata, (LICS, (2009), IEEE Computer Society), 167-176
[9] Chadha, R.; Kremer, S.; Scedrov, A., Formal analysis of multiparty contract signing, J. Autom. Reason., 36, 1-2, 39-83, (2006) · Zbl 1134.94372
[10] Chatterjee, K.; Doyen, L.; Henzinger, T. A.; Raskin, J.-F., Algorithms for omega-regular games with imperfect information, Log. Methods Comput. Sci., 3, 3, (2007) · Zbl 1125.91028
[11] Chatterjee, K.; Henzinger, T. A.; Jurdzinski, M., Games with secure equilibria, Theor. Comput. Sci., 365, 1-2, 67-82, (2006) · Zbl 1108.91007
[12] Chatterjee, K.; Henzinger, T. A.; Piterman, N., Strategy logic, Inf. Comput., 208, 6, 677-693, (2010) · Zbl 1205.68197
[13] Chatterjee, K.; Henzinger, T. A.; Piterman, N., Generalized parity games, (FoSSaCS, LNCS, vol. 4423, (2007), Springer), 153-167 · Zbl 1195.68053
[14] Da Costa Lopes, A.; Laroussinie, F.; Markey, N., ATL with strategy contexts: expressiveness and model checking, (FSTTCS, LIPIcs, vol. 8, (2010)), 120-132 · Zbl 1245.68135
[15] Emerson, E. A.; Jutla, C., Tree automata, mu-calculus and determinacy, (FOCS, (1991), IEEE Comp. Soc.), 368-377
[16] Emerson, E. A.; Lei, C.-L., Modalities for model checking: branching time strikes back, (POPL, (1985)), 84-96
[17] Fijalkow, N.; Horn, F., The surprizing complexity of reachability games, (2010), CoRR
[18] Filiot, Emmanuel; Jin, Naiyong; Raskin, Jean-François, An antichain algorithm for LTL realizability, (CAV 2009, Lecture Notes in Computer Science, vol. 5643, (2009), Springer), 263-277 · Zbl 1242.68158
[19] Filiot, Emmanuel; Jin, Naiyong; Raskin, Jean-François, Antichains and compositional algorithms for LTL synthesis, Form. Methods Syst. Des., 39, 3, 261-296, (2011) · Zbl 1258.03046
[20] Finkbeiner, Bernd; Schewe, Sven, Bounded synthesis, Int. J. Softw. Tools Technol. Transf., 15, 5-6, 519-539, (2013) · Zbl 1141.68491
[21] Fisman, D.; Kupferman, O.; Lustig, Y., Rational synthesis, (Proc. of TACAS, LNCS, vol. 6015, (2010), Springer), 190-204 · Zbl 1284.68396
[22] (Grädel, E.; Thomas, W.; Wilke, T., Automata, Logics, and Infinite Games: A Guide to Current Research, LNCS, vol. 2500, (2002), Springer) · Zbl 1011.00037
[23] Immerman, N., Number of quantifiers is better than number of tape cells, J. Comput. Syst. Sci., 22, 384-406, (1981) · Zbl 0486.03019
[24] Jamroga, W.; Mauw, S.; Melissen, M., Fairness in non-repudiation protocols, (Proc. of STM, LNCS, vol. 7170, (2012), Springer), 122-139
[25] Kremer, S.; Raskin, J.-F., A game-based verification of non-repudiation and fair exchange protocols, J. Comput. Secur., 11, 3, 399-430, (2003)
[26] Kupferman, O.; Vardi, M. Y., Safraless decision procedures, (FOCS, (2005))
[27] Martin, D., Borel determinacy, Ann. Math., 102, 363-371, (1975) · Zbl 0336.02049
[28] Mogavero, F.; Murano, A.; Perelli, G.; Vardi, M. Y., What makes ATL* decidable? A decidable fragment of strategy logic, (CONCUR, (2012)), 193-208 · Zbl 1365.68329
[29] Mogavero, F.; Murano, A.; Vardi, M. Y., Reasoning about strategies, (Proc. of FSTTCS, LIPIcs, vol. 8, (2010), Schloss Dagstuhl - LZfI), 133-144 · Zbl 1245.68138
[30] Nash, J. F., Equilibrium points in n-person games, Proc. Natl. Acad. Sci. USA, 36, 48-49, (1950) · Zbl 0036.01104
[31] Piterman, N., From nondeterministic Büchi and streett automata to deterministic parity automata, Log. Methods Comput. Sci., 3, 3, (2007) · Zbl 1125.68067
[32] Piterman, N.; Pnueli, A., Faster solutions of rabin and streett games, (LICS, (2006)), 275-284
[33] Pnueli, A.; Rosner, R., On the synthesis of a reactive module, (POPL, (1989), ACM Press), 179-190
[34] Rabin, M. O., Decidability of second-order theories and automata on infinite trees, Trans. Am. Math. Soc., 141, 1-35, (1969) · Zbl 0221.02031
[35] Ramadge, P. J.; Wonham, W. M., Supervisory control of a class of discrete event processes, SIAM J. Control Optim., 25, 1, 206-230, (1987) · Zbl 0618.93033
[36] Safra, Shmuel, On the complexity of omega-automata, (29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24-26 October 1998, (1988), IEEE Computer Society), 319-327
[37] Shapley, L. S., Stochastic games, Proc. Natl. Acad. Sci. USA, 39, 1095-1100, (1953) · Zbl 0051.35805
[38] Ummels, M.; Wojtczak, D., The complexity of Nash equilibria in stochastic multiplayer games, Log. Methods Comput. Sci., 7, 3, (2011) · Zbl 1238.91025
[39] Wang, F.; Huang, C.; Yu, F., A temporal logic for the interaction of strategies, (Proc. of CONCUR, LNCS, vol. 6901, (2011), Springer), 466-481 · Zbl 1343.68157
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.