Maximally Permissive Strategies for Safety Properties

Question

Different definitions of maximally permissive strategies exist. For instance, in (Bernet, Janin, and Walukiewicz 2002), strategies are compared by looking at inclusion of the behaviors/outcomes they allow. In particular, a maximally permissive strategy N is a non-deterministic strategy such that there is no other non-deterministic strategy N_1 that allows more behaviors/outcomes than N.

Moreover, it is known that in a safety game Player 0 (let's call it the protagonist) has a maximally permissive strategy. It is also known that if a game G has a maximal permissive strategy then G can be reduced to a safety game.

My question is: there should be a theorem claiming the existence of maximally permissive strategies for safety properties, is it proved in some paper?

Answer 1

In a safety game, the existence of a maximally permissive strategy is easy to show: you always allow all moves that stay in the winning region. This works because safety games are precisely the games where a play staying in the winning region is guaranteed to be winning itself. Moreover such a strategy is clearly maximally permissive, by definition of the winning region.