Shield Synthesis
Definition
Shield synthesis constructs a runtime component that monitors a system’s inputs and outputs and corrects outputs that would violate a safety specification, while minimizing unnecessary deviation from the original system.
Why It Matters
It gives a formally synthesized enforcement layer when the original controller is too complex, opaque, incomplete, third-party, or learned. The shield can be certified against a small critical specification even when the whole design cannot be fully verified.
Formalism / Key Objects
- A design
Dhas input alphabetSigma_I, output alphabetSigma_O, and transition/output behavior. - A shield
Sobserves the input/output stream ofDand emits corrected outputs so the compositionD o Ssatisfies a property setphi. - A generic shield works for any design satisfying a trusted valid subset
phi_v. - Correctness requires the shielded system to satisfy the critical properties.
- Minimum interference is captured by comparing output trace distance against language-distance violation severity.
- K-Stabilizing Shield Synthesis gives a concrete safety-game construction for bounded recovery after unavoidable violations.
- Safety Games are the underlying game-solving pattern when the specification is safety-shaped.
Connections
- Bloem2015 - Shield Synthesis is the core reactive-systems source for this concept.
- Alshiekh2018 - Safe Reinforcement Learning via Shielding adapts the shielding idea to RL action filtering.
- Runtime Verification monitors executions; shield synthesis adds corrective control.
- Formal Methods supplies the automata, safety games, and synthesis machinery.
- Reactive Synthesis is the broader offline controller-synthesis setting; shield synthesis is narrower because it corrects an existing design.
Common Confusions
- A shield is not the same as a monitor if it can actively modify outputs or actions.
- Generic shield synthesis may ignore the implementation, but it still relies on a trusted specification boundary.
- Minimum interference does not mean zero interference; it means deviations are justified by unavoidable or realized safety risk.