Hostname: page-component-586b7cd67f-2brh9 Total loading time: 0 Render date: 2024-11-26T13:15:53.596Z Has data issue: false hasContentIssue false

Permissive strategies: from parity games to safety games

Published online by Cambridge University Press:  15 December 2002

Julien Bernet
Affiliation:
LaBRI – CNRS – Université de Bordeaux I, 351 cours de la Libération, 33405 Talence Cedex, France; [email protected]. [email protected].
David Janin
Affiliation:
LaBRI – CNRS – Université de Bordeaux I, 351 cours de la Libération, 33405 Talence Cedex, France; [email protected]. [email protected].
Igor Walukiewicz
Affiliation:
LaBRI – CNRS – Université de Bordeaux I, 351 cours de la Libération, 33405 Talence Cedex, France; [email protected]. [email protected].
Get access

Abstract

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.

Keywords

Type
Research Article
Copyright
© EDP Sciences, 2002

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

A. Arnold, A. Vincent and I. Walukiewicz, Games for synthesis of controllers with partial observation. Theoret. Comput. Sci. (to appear).
Bergeron, A., A unified approach to control problems in discrete event processes. RAIRO: Theoret. Informatics Appl. 27 (1993) 555-573.
Buchi, J.R., State strategies for games in $F_{\sigma\delta}\cap G_{\delta\sigma}$ . J. Symbolic Logic 48 (1983) 1171-1198. CrossRef
C.G. Cassandras and S. Lafortune, Introduction to Discrete Event Systems. KluwerAcademic Publishers (1999).
S. Dziembowski, M. Jurdzinski and I. Walukiewicz, How much memory is needed to win infinite games, in LICS (1997) 99-110.
E.A. Emerson, C. Jutla and A. Sistla, On model-checking for fragments of µ-calculus, in CAV'93. Springer, Lecture Notes in Comput. Sci. 697 (1993) 385-396.
E.A. Emerson and C.S. Jutla, Tree automata, mu-calculus and determinacy, in Proc. FOCS 91 (1991) 368-377.
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).
Y. Gurevich and L. Harrington, Trees, automata and games, in 14th ACM Symp. on Theory of Computations (1982) 60-65.
Jurdzinski, M., Deciding the winner in parity games is in UP ∩ co-UP. Inform. Process. Lett. 68 (1998) 119-124. CrossRef
M. Jurdzinski, Small progress measures for solving parity games, in STACS. Springer, Lecture Notes in Comput. Sci. 1770 (2000) 290-301.
O. Kupferman, M.Y. Vardi and P. Wolper, An automata-theoretic approach to branching-time model checking. J. ACM 47 (2000).
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.
Mostowski, A.W., Hierarchies of weak automata and week monadic formulas. Theoret. Comput. Sci. 83 (1991) 323-335. CrossRef
P.J.G. Ramadge and W.M. Wonham, The control of discrete event systems. Proc. of IEEE 77 (1989).
W. Thomas, Automata on infinite objects, edited by J. van Leeuven. Elsevier, Handb. Theoret. Comput. Sci. B (1990) 133-192.
W. Thomas, On the synthesis of strategies in infinite games, in STACS '95. Springer, Lecture Notes in Comput. Sci. 900 (1995) 1-13.
W. Thomas, Languages, automata, and logic, edited by G. Rozenberg and A. Salomaa. Springer-Verlag, Handbook Formal Languages 3 (1997).
J. Vöge and M. Jurdzinski, A discrete strategy improvement algorithm for solving parity games (Extended abstract), in CAV. Springer, Lecture Notes in Comput. Sci. 1855 (2000) 202-215.
Zielonka, W., Infinite games on finitely coloured graphs with applications to automata on infinte trees. Theoret. Comput. Sci. 200 (1998) 135-183. CrossRef
Zwick, U. and Paterson, M., The complexity of mean payoff games on graps. Theoret. Comput. Sci. 158 (1996) 343-359. CrossRef