K-Stabilizing Shield Synthesis

Context

Bloem2015 - Shield Synthesis defines generic shields for reactive systems and then gives a concrete construction for k-stabilizing shields. The construction enforces safety immediately while bounding how long the shield may deviate from the original design after an unavoidable violation.

Formal Statement

Let phi=phi_v union (phi \ phi_v) be a safety specification with trusted valid subset phi_v. A generic shield S must work for any design D satisfying phi_v and guarantee:

$$(D\circ S)\models \varphi .$$

Minimum interference is expressed with:

• output trace distance d_sigma, measuring shield deviation from design output;
• language distance d_L, measuring how badly the design trace violates phi.

An optimal generic shield ensures correctness and:

$$d_{\sigma }({\sigma }_O,S({\sigma }_I\Vert {\sigma }_O))\le d_L(L(\varphi ),{\sigma }_I\Vert {\sigma }_O).$$

A k-stabilizing shield may deviate for at most k consecutive steps once a violation becomes unavoidable. If a second violation occurs during recovery, the shield enters fail-safe mode: correctness remains required, but minimum-deviation tracking is abandoned.

Derivation / Construction

• Translate critical safety properties into safety automata.
• Build a violation monitor that detects when violation is unavoidable and maintains a recovery counter c.
• Build a monitor for the valid subset phi_v, exploiting the assumption that the design satisfies it.
• Build a deviation monitor that records whether the shield output differs from the design output.
• Construct the safety game as the product of violation, valid-subset, deviation, and full-property monitors.
• The safe states enforce the full property and allow deviations only during the k-step recovery window or fail-safe mode.
• Solve the safety game for a winning strategy; if none exists, increase k and retry.

Implications

• The shield can be synthesized without analyzing the full implementation, which supports third-party components and changing designs.
• Minimum interference is formal: the shield cannot deviate before violation is unavoidable.
• The fail-safe mode makes explicit a practical trade-off between bounded recovery and guaranteed correctness.
• Later RL shielding inherits this logic but changes the interface from reactive-system outputs to learner actions.

Links

• Source: Bloem2015 - Shield Synthesis
• Concepts: Shield Synthesis, Shielding, Runtime Verification