Safe Policy Invariance

Abstract

A policy selecting only controls whose possible responses stay in the safe kernel preserves the kernel and safety.

Theorem 1.1 (Safe policies preserve the safe kernel).

$$\begin{array}{c}{K}^{\ast }\subseteq S,\\ U_{safe}(x):=\{u\in U(x)\mid \forall y,R\left(x,u,y\right)\Rightarrow y\in K^{\ast }\},\\ \forall x,pi(x)\in U_{safe}(x)\\ \Rightarrow \forall x_0,x_t,x_0\in K^{\ast }\wedge \mathrm{Reachable}\left(\mathrm{PolicyStep}\left(R,pi\right),x_0,x_t\right)\\ \Rightarrow x_t\in K^{\ast }\wedge x_t\in S.\end{array}$$

Proof. Machine-checked in Lean as D5/S0/Rewriting/Safety/SafePolicyInvariant.safe_policy_preserves_kernel (✓ std3). ∎

Source. Repository-derived.

Commentary.

For each state, the safe-control set is constructed from the available controls and the response relation: every possible successor must lie in the safe kernel.

The policy-induced transition relation is passed directly to the canonical invariant-safety theorem. Every finitely reachable state therefore lies in the kernel and, by inclusion, in S.

References

• Truth anchor: D5/S0/Rewriting/Safety/SafePolicyInvariant.safe_policy_preserves_kernel
• Dependency: D5/S0/Rewriting/Safety/InvariantSafety