Reachability Safety Dichotomy

Abstract

A relation-generated least fixed point either certifies all finite paths as safe or supplies a finite path to a bad state.

Theorem 1.1 (Safety and finite counterexample paths form a dichotomy).

$$\begin{gathered} \forall X:Type, \\ R:\mathrm{Set}\left(X\times X\right),I_0,S:\mathrm{Set}\left(X\right), \\ (\mathrm{lfp}\left(\mathrm{reachStep}\left(R,I_0\right)\right)\subseteq S\Rightarrow \forall x_0\in I_0,x:X,\mathrm{ReflTransGen}\left(R,x_0,x\right)\Rightarrow x\in S)\wedge \\ (\mathrm{Nonempty}\left(\mathrm{inter}\left(\mathrm{lfp}\left(\mathrm{reachStep}\left(R,I_0\right)\right),X\setminus S\right)\right)\Rightarrow \exists x_0\in I_0,x\in X\setminus S,\mathrm{ReflTransGen}\left(R,x_0,x\right)). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S1/FixedPoints/Reachability/SafetyDichotomy.reachability_safety_and_bad_path (✓ std3). ∎

Source. Repository-derived.

Commentary.

A transition relation R and initial set I0 construct the reachability operator by adjoining I0 to the direct R-image of the current approximation. Reach is the least fixed point of this operator.

If Reach is contained in the safe set S, every finite reflexive-transitive R-path beginning in I0 ends in S. This is the path-level safety clause of the source theorem.

If Reach meets the complement of S, finite-stage expansion locates the bad state at a finite iterate. Induction over that iterate constructs an initial state and a finite R-path ending outside S.

The proof imports the canonical relation-generated reachability operator and its finite-stage expansion rather than redeclaring either source object. The pinned relation closure constructors supply the exact finite path.

References

• Truth anchor: D5/S1/FixedPoints/Reachability/SafetyDichotomy.reachability_safety_and_bad_path
• Dependency: D5/S1/FixedPoints/RelationalReachExpansion