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?