Safety Games
Definition
A safety game is a two-player game in which the controller wins by keeping the play inside a safe region forever, regardless of the environment’s moves.
Why It Matters
Safety games are the operational bridge between temporal safety specifications and executable control or shielding policies. They are simpler than parity games and often support greatest-fixpoint or reachability-style algorithms.
Formalism / Key Objects
- A safety game has states
S, environment moves, controller moves, a transition relation or function, and a safe setF subseteq S. - For input variables
X, output variablesY, and transition functiondelta, a predecessor operator has the schematic form
- The controller winning region is the greatest fixed point
- A state is winning if the controller has a strategy that remains in the fixed point forever.
Connections
- Reactive Synthesis reduces Safety LTL realizability to safety-game solving in restricted settings.
- Shield Synthesis constructs runtime enforcers by solving safety games over monitor products.
- Centralized and Factored MARL Shielding treats the agents’ proposed joint action as the controllable move in a safety game.
- Invariant Synthesis can be seen as searching for symbolic summaries of winning safety regions.
- Safety LTL Automata and Games records the bad-prefix automata route into safety games.
Common Confusions
- A safety game is not merely a game with a safety-themed reward; the winning condition is prefix-closed avoidance of losing states.
- Reachability and safety games are dual for realizability, but strategy extraction and implementation details may differ.
- Solving the safety game still requires a trusted abstraction of state, observation, and controllable action.