Permissive strategies : from parity games to safety games

Bernet, Julien; Janin, David; Walukiewicz, Igor

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 36 (2002) no. 3, pp. 261-275.

It is proposed to compare strategies in a parity game by comparing the sets of behaviours they allow. For such a game, there may be no winning strategy that encompasses all the behaviours of all winning strategies. It is shown, however, that there always exists a permissive strategy that encompasses all the behaviours of all memoryless strategies. An algorithm for finding such a permissive strategy is presented. Its complexity matches currently known upper bounds for the simpler problem of finding the set of winning positions in a parity game. The algorithm can be seen as a reduction of a parity to a safety game and computation of the set of winning positions in the resulting game.

[1] A. Arnold, A. Vincent and I. Walukiewicz, Games for synthesis of controllers with partial observation. Theoret. Comput. Sci. (to appear). | MR

[2] A. Bergeron, A unified approach to control problems in discrete event processes. RAIRO: Theoret. Informatics Appl. 27 (1993) 555-573. | Numdam | MR | Zbl

[3] J.R. Buchi, State strategies for games in $F_{\sigma \delta }\cap G_{\delta \sigma }$. J. Symbolic Logic 48 (1983) 1171-1198. | MR | Zbl

[4] C.G. Cassandras and S. Lafortune, Introduction to Discrete Event Systems. Kluwer Academic Publishers (1999). | MR | Zbl

[5] S. Dziembowski, M. Jurdzinski and I. Walukiewicz, How much memory is needed to win infinite games, in LICS (1997) 99-110.

[6] E.A. Emerson, C. Jutla and A. Sistla, On model-checking for fragments of $\mu$-calculus, in CAV'93. Springer, Lecture Notes in Comput. Sci. 697 (1993) 385-396.

[7] E.A. Emerson and C.S. Jutla, Tree automata, mu-calculus and determinacy, in Proc. FOCS 91 (1991) 368-377.

[8] O. Grumberg, T. Heyman and A. Schusterk, Distributed symbolic model checking for mu-calculus, in CAV'01. Springer, Lecture Notes in Comput. Sci. 2102 (2001). | Zbl

[9] Y. Gurevich and L. Harrington, Trees, automata and games, in 14th ACM Symp. on Theory of Computations (1982) 60-65.

[10] M. Jurdziński, Deciding the winner in parity games is in UP$\cap$co-UP. Inform. Process. Lett. 68 (1998) 119-124. | MR | Zbl

[11] M. Jurdziński, Small progress measures for solving parity games, in STACS. Springer, Lecture Notes in Comput. Sci. 1770 (2000) 290-301. | MR | Zbl

[12] O. Kupferman, M.Y. Vardi and P. Wolper, An automata-theoretic approach to branching-time model checking. J. ACM 47 (2000). | MR | Zbl

[13] A.W. Mostowski, Regular expressions for infinite trees and a standard form of automata, edited by A. Skowron, in Fifth Symposium on Computation Theory. Springer, Lecture Notes in Comput. Sci. 208 (1984) 157-168. | MR | Zbl

[14] A.W. Mostowski, Hierarchies of weak automata and week monadic formulas. Theoret. Comput. Sci. 83 (1991) 323-335. | MR | Zbl

[15] P.J.G. Ramadge and W.M. Wonham, The control of discrete event systems. Proc. of IEEE 77 (1989).

[16] W. Thomas, Automata on infinite objects, edited by J. van Leeuven. Elsevier, Handb. Theoret. Comput. Sci. B (1990) 133-192. | MR | Zbl

[17] W. Thomas, On the synthesis of strategies in infinite games, in STACS '95. Springer, Lecture Notes in Comput. Sci. 900 (1995) 1-13. | MR

[18] W. Thomas, Languages, automata, and logic, edited by G. Rozenberg and A. Salomaa. Springer-Verlag, Handbook Formal Languages 3 (1997). | MR

[19] J. Vöge and M. Jurdziński, A discrete strategy improvement algorithm for solving parity games (Extended abstract), in CAV. Springer, Lecture Notes in Comput. Sci. 1855 (2000) 202-215. | Zbl

[20] W. Zielonka, Infinite games on finitely coloured graphs with applications to automata on infinte trees. Theoret. Comput. Sci. 200 (1998) 135-183. | MR | Zbl

[21] U. Zwick and M. Paterson, The complexity of mean payoff games on graps. Theoret. Comput. Sci. 158 (1996) 343-359. | MR | Zbl