Abstract
We consider games where the winning conditions are disjunctions (or dually, conjunctions) of parity conditions; we call them generalized parity games. These winning conditions, while ω-regular, arise naturally when considering fair simulation between parity automata, secure equilibria for parity conditions, and determinization of Rabin automata. We show that these games retain the computational complexity of Rabin and Streett conditions; i.e., they are NP-complete and co-NP-complete, respectively. The (co-)NP-hardness is proved for the special case of a conjunction/disjunction of two parity conditions, which is the case that arises in fair simulation and secure equilibria. However, considering these games as Rabin or Streett games is not optimal. We give an exposition of Zielonka’s algorithm when specialized to this kind of games. The complexity of solving these games for k parity objectives with d priorities, n states, and m edges is \(O(n^{2 k d} \cdot m) \cdot \frac{(k\cdot d)!}{d!^k}\), as compared to O(n 2 kd ·m) ·(k·d)! when these games are solved as Rabin/Streett games. We also extend the subexponential algorithm for solving parity games recently introduced by Jurdziński, Paterson, and Zwick to generalized parity games. The resulting complexity of solving generalized parity games is \(n^{O(\sqrt{n})} \cdot \frac{(k\cdot d)!}{d!^k}\). As a corollary we obtain an improved algorithm for Rabin and Streett games with d pairs, with time complexity \(n^{O(\sqrt{n})} \cdot d!\).
This research was supported in part by the Swiss National Science Foundation, and by the NSF grants CCR-0225610 and CCR-0234690.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bustan, D., Grumberg, O.: Simulation based minimization. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 255–270. Springer, Heidelberg (2000)
Chatterjee, K., Henzinger, T.A., Jurdziński, M.: Games with secure equilibria. In: LICS, pp. 160–169. IEEE Computer Society Press, Los Alamitos (2004)
Chatterjee, K., Henzinger, T.A., Piterman, N.: Generalized parity games. Technical Report: UC Berkeley EECS-2006-144 (2006)
Dill, D.L., Hu, A.J., Wong-Toi, H.: Checking for language inclusion using simulation relations. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 255–265. Springer, Heidelberg (1992)
Dziembowski, S., Jurdziński, M., Walukiewicz, I.: How much memory is needed to win infinite games. In: LICS, pp. 99–110. IEEE Computer Society Press, Los Alamitos (1997)
Emerson, E.A., Jutla, C.: The complexity of tree automata and logics of programs. In: FOCS, pp. 328–337. IEEE Computer Society Press, Los Alamitos (1988)
Emerson, E.A., Jutla, C.: Tree automata, μ-calculus and determinacy. In: FOCS, pp. 368–377. IEEE Computer Society Press, Los Alamitos (1991)
Etessami, K., Holzmann, G.: Optimizing Büchi automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 153–167. Springer, Heidelberg (2000)
Henzinger, T.A., Kupferman, O., Rajamani, S.: Fair simulation. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 273–287. Springer, Heidelberg (1997)
Horn, F.: Streett games on finite graphs. In: Games in Design and Verification (2005)
Jurdziński, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290–301. Springer, Heidelberg (2000)
Jurdziński, M., Paterson, M., Zwick, U.: A deterministic subexponential algorithm for solving parity games. In: SODA, pp. 117–123. ACM, New York (2006)
Martin, D.A.: Borel determinacy. Annals of Mathematics 65, 363–371 (1975)
Milner, R.: An algebraic definition of simulation between programs. In: Second International Joint Conference on Artificial Intelligence, pp. 481–489. The British Computer Society (1971)
Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. In: LICS, pp. 255–264. IEEE Computer Society Press, Los Alamitos (2006)
Piterman, N., Pnueli, A.: Faster solution of rabin and streett games. In: LICS, pp. 275–284. IEEE Computer Society Press, Los Alamitos (2006)
Rabin, M.O.: Decidability of second order theories and automata on infinite trees. Transaction of the AMS 141, 1–35 (1969)
Ramadge, P.J.G., Wonham, W.M.: The control of discrete event systems. IEEE Transactions on Control Theory 77, 81–98 (1989)
Safra, S.: On the complexity of ω-automata. In: FOCS, pp. 319–327. IEEE Computer Society Press, Los Alamitos (1988)
Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248–263. Springer, Heidelberg (2000)
Streett, R.S.: Propositional dynamic logic of looping and converse. Information and Control 54, 121–141 (1982)
Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science 200(1–2), 135–183 (1998)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Chatterjee, K., Henzinger, T.A., Piterman, N. (2007). Generalized Parity Games. In: Seidl, H. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2007. Lecture Notes in Computer Science, vol 4423. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71389-0_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-71389-0_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71388-3
Online ISBN: 978-3-540-71389-0
eBook Packages: Computer ScienceComputer Science (R0)