Skip to content

Recovery and Progress Analysis

This document explains why the four recovery claim levels exist and how the universal attractor algorithm establishes them. It is aimed at engineers who want to understand the mathematical model and design rationale, not at those looking for step-by-step instructions.

For step-by-step instructions, see how-to/prove-safe-recovery.md. For the normative definitions, see reference/assurance.md.

Four Questions About Recovery

When an SSFC must recover from a fault state to a safe state, we can ask four increasingly strong questions:

  1. STRUCTURAL: Is there any path at all in the state machine topology? (Guards ignored.)
  2. POSSIBLE: Is there at least one execution where the system reaches the safe state? (Guards satisfiable?)
  3. GUARANTEED: Will the system always reach the safe state, on every admissible execution?
  4. BOUNDED: How many scans does it take, in the worst case?

These correspond exactly to the four claim levels produced by analyze_recovery(). Each is strictly stronger than the one before.

The Pasteurizer Example

SSFC Pasteurizer
  STEP Production  → SafeStopped  WHEN abort_signal
  STEP SafeStopped → Idle         WHEN reset_request

For the transition Production → SafeStopped:

STRUCTURAL:  PROVED          (path exists: Production → SafeStopped)
POSSIBLE:    PROVED          (abort_signal is SAT)
GUARANTEED:  PROVED-COND     (requires ASSUME abort_signal)
BOUNDED:     PROVED-COND     within 1 scan

For the transition SafeStopped → Idle, where reset_request is not assumed:

STRUCTURAL:  PROVED          (path exists)
POSSIBLE:    PROVED          (reset_request is SAT)
GUARANTEED:  NOT PROVED      (no ASSUME for reset_request; system may wait indefinitely)
BOUNDED:     NOT PROVED

The gap between POSSIBLE and GUARANTEED is not a defect in the analysis. It is the correct answer: the system can eventually reach Idle, but without an operator guarantee to press the reset button, the analysis cannot promise it will.

STRUCTURAL: The Topology Floor

STRUCTURAL checks whether a path exists in the marking graph from the source marking set to the home marking set, ignoring all transition guards entirely. It is the minimum necessary condition.

If STRUCTURAL is NOT PROVED, no execution can ever reach home. The topology itself prevents it — wrong wiring, a missing transition, or a parallel JOIN whose inputs can never all be active simultaneously. This is a hard structural defect that cannot be fixed by adding ASSUME clauses or adjusting guard logic.

STRUCTURAL PROVED does not imply anything about whether guards ever allow the path to be taken. A system can have a valid path in the topology but have guards that are never satisfiable under any input.

POSSIBLE: Existence of an Admissible Execution

POSSIBLE checks SAT(guard ∧ assumes) for each transition along some path from source to home. If every step on some path is guard-satisfiable, a feasible execution might exist.

The Per-Edge SAT Abstraction

POSSIBLE uses a per-edge SAT abstraction: each transition's guard is checked independently against the ASSUME clauses. This does not verify that the guards are satisfiable simultaneously in the correct sequence across multiple scans — data values can persist across scans in ways that make individual SAT checks optimistic.

POSSIBLE is therefore an over-approximation:

  • POSSIBLE = NOT PROVED does not mean the path is infeasible. A more complex data trajectory might still achieve it.
  • POSSIBLE = PROVED does not guarantee a coherent execution definitely exists; each guard was only checked in isolation.

In practice, for boolean guard structures this approximation is tight: if each boolean guard is individually satisfiable, a combined feasible execution almost always exists. For SSFCs with complex arithmetic guards spanning multiple transitions, POSSIBLE PROVED should be read as "likely feasible, not fully verified." The following claim levels — GUARANTEED and BOUNDED — provide the stronger, verified assurances.

GUARANTEED: Universal Attractor Analysis

GUARANTEED is the hardest claim: every admissible execution (satisfying all ASSUMEs) eventually reaches home.

Why Finding One Good Path Is Not Enough

GUARANTEED cannot be proved by finding a single path on which the system reaches home. It must rule out all bad paths — every possible way the environment could provide inputs to divert or stall the system. The universal attractor construction does this by reasoning about all successors simultaneously.

PossibleSucc: The Complete Transition Relation

For a marking M, define:

PossibleSucc(M) = { M′ | ∃ input: SAT(guard(t) ∧ assumes) for transition t: M → M′ }

This is the set of all markings the system could reach in one scan from M, over all inputs that satisfy the ASSUME clauses. It captures everything the environment could cause — not just what it will cause on some particular run.

The No-Stall Condition

A marking M is "no-stall" if:

UNSAT(assumes ∧ ¬g₁ ∧ … ∧ ¬gₙ)

where g₁…gₙ are all outgoing guards from M. Equivalently: under the ASSUME clauses, it is impossible for all guards to be simultaneously false. The system cannot idle in M indefinitely — some transition always fires.

If M is not no-stall, there exists an admissible input under which M has no enabled transition. The system simply waits in M forever. No GUARANTEED proof can span M.

The Universal Attractor Construction

The attractor is built by the following fixed-point computation:

Attr₀     = home_marks
Attr_{k+1} = Attr_k ∪ { M | no_stall(M)
                              ∧ PossibleSucc(M) ≠ ∅
                              ∧ PossibleSucc(M) ⊆ Attr_k }

A marking M joins the attractor when two conditions hold simultaneously:

  1. It cannot stall (some transition always fires under ASSUMEs).
  2. Every possible successor is already in the attractor.

The fixed point terminates because: - The marking set is finite. - The attractor grows monotonically (markings are never removed).

The attractor sub-graph is always a DAG: a cycle would require two markings M and M′ where M needs M′ already in the attractor and M′ needs M already in the attractor. Since markings enter the attractor in order of the round k in which they are first included, a cycle would force both to have entered before the other — a contradiction.

Soundness

The construction is sound by induction on the round k:

  • Base (k = 0): home ∈ Attr₀ by construction. Reaching home takes 0 additional scans.
  • Step: Suppose every marking in Attr_k reaches home in at most k scans. Take any M ∈ Attr_{k+1} \ Attr_k. By construction, no_stall(M) holds, so some transition fires each scan. Every possible successor is in Attr_k, so each successor reaches home in at most k more scans. Therefore M reaches home in at most k + 1 scans.
  • Conclusion: From any M ∈ Attr, every admissible execution reaches home in finitely many scans.

GUARANTEED = PROVED means source_marks ⊆ Attr. GUARANTEED = NOT PROVED means at least one source marking is outside the attractor.

Why "Always-Enabled Subgraph" Is Wrong

An earlier (incorrect) approach to GUARANTEED only kept transitions whose guards were always enabled — i.e., transitions for which VALID(assumes → guard) holds. This is fundamentally flawed.

The always-enabled subgraph is an under-approximation of PossibleSucc: it excludes transitions that are sometimes enabled under ASSUMEs but not always. For a ∀ claim, we must consider all transitions that could fire (SAT-based), because a sometimes-enabled transition that leads to a non-home state is a genuine threat to GUARANTEED, even if a tautologically-enabled transition to home also exists from the same marking.

Counterexample: Consider:

STEP Fault → Safe    WHEN TRUE
STEP Fault → Trouble WHEN bad_signal

The always-enabled subgraph keeps only the TRUE-guarded edge and incorrectly reports GUARANTEED PROVED. The universal attractor includes Trouble in PossibleSucc(Fault) and correctly checks whether Trouble ∈ Attr. If it is not (because Trouble has no outgoing transitions), GUARANTEED is NOT PROVED. The system might go to Trouble instead of Safe, and once there it is stuck.

BOUNDED: Worst-Case Scan Count

BOUNDED asks: given that GUARANTEED holds, how many scans does the worst-case admissible execution take?

Attractor Rank

Define the attractor rank B(M) by:

B(home) = 0
B(M)    = 1 + max_{M′ ∈ PossibleSucc(M)} B(M′),   for M ∈ Attr \ home

Because the attractor is a DAG, this recursion is well-founded — no cycles prevent termination of the recursion. Because no_stall(M) holds for every M in the attractor, each scan fires a transition, so the scan count equals the transition count along any path.

BOUNDED is then:

BOUNDED = max_{M ∈ source_marks ∩ Attr} B(M)

Why Minimum BFS Depth Is Wrong

For a branching SSFC with two paths from Start to Home:

Start → Home          (1 transition)
Start → Middle → Home (2 transitions)

The minimum (BFS) depth is 1. But if the environment can always choose to take the longer path, the worst case is 2. BOUNDED must give the maximum depth over all possible choices the environment could make, because a safety argument must hold even when the environment acts adversarially within the ASSUME constraints.

Assumption Provenance: Load-Bearing ASSUMEs

When GUARANTEED is PROVED-CONDITIONAL, the assumptions_used field lists only the load-bearing ASSUME clauses — those whose removal would cause GUARANTEED to fail.

The Deletion Test

For each ASSUME clause aᵢ, remove it from the ASSUME set and recompute the universal attractor. If source_marks ⊄ Attr after removal, aᵢ is load-bearing. The assumptions_used list is the minimal set needed to sustain the GUARANTEED proof.

Engineering Significance

An ASSUME clause that is not load-bearing does not contribute to the GUARANTEED proof. It may still be required for other claims — for example, it may be needed to keep a guard SAT-satisfiable for POSSIBLE — but its presence is not necessary for the ∀ argument. During engineering review, load-bearing ASSUMEs are the clauses that require the most scrutiny: each one represents an obligation that must be discharged by the system's physical environment, operator procedure, or higher-level control logic.

Parallel Regions

For SSFCs with PARALLEL/REGION/JOIN constructs, markings are frozensets of active places across all regions simultaneously. Analysis operates on these combined markings, not on individual regions in isolation.

A JOIN condition such as:

JOIN FROM HeatDone, MixDone TO Completed

fires only when both HeatDone and MixDone are simultaneously active. The no_stall condition is checked over the full combined marking; PossibleSucc considers all transitions that can fire from any active region at once.

If one region stalls — for example, its transition guard is not satisfiable under the current ASSUMEs — the combined marking is not in the no-stall set. GUARANTEED is NOT PROVED for that combined marking even if the other region has a guaranteed progression path. The analysis reflects the physical reality: the SSFC as a whole is stuck if any one region is stuck.

What NOT-PROVED Means

GUARANTEED = NOT PROVED is a design finding, not a solver failure or an analysis limitation.

It means one or more of the following:

  • A reachable marking lies outside the attractor because it can stall (some input under ASSUMEs disables all outgoing guards).
  • A reachable marking lies outside the attractor because at least one of its possible successors leads to a non-home sink — a state the system can reach but from which home is unreachable.
  • The ASSUME clauses are insufficient: they fail to establish no_stall for some marking that must be in the attractor for the proof to close.

The reason field in RecoveryEvidence names the specific marking and the nature of the problem. This gives three actionable responses:

  1. Add a justified ASSUME clause. If an external guarantee (operator procedure, interlock signal) can establish no-stall for the offending marking, add it as an ASSUME and re-run the analysis.
  2. Redesign the state machine. Remove or redirect the stall path or non-home sink so that the topology itself prevents the problematic execution.
  3. Accept and document. If GUARANTEED cannot be established — and the design rationale accepts this — document why POSSIBLE suffices and what engineering controls compensate for the absence of a universal guarantee.

The goal of the analysis is not to force PROVED on every claim. It is to make the actual assurance level precise and legible, so that engineering decisions rest on a clear statement of what has and has not been verified.