Safety Horizon Semantics¶

Current default: time-free infinite-horizon reachability¶

The shield's Bellman objective is

Pr(eventually visit Unsafe | current state, shield policy)

over the time-free induced transition graph. SoundVIResult.q is an upper bound on minimal eventual-unsafe reachability in that graph; it is not a finite-episode violation count and it does not stop at the simulator's max_steps value.

All current exact and learned shield graph paths use the public Markov state width and omit hidden time counters. Consequently, every current environment's main shield solve targets infinite-horizon safety:

This is the paper-facing default and should remain so. A finite rollout is an observation window for an infinite-horizon objective, not a change to the shield's Bellman horizon.

What the learned certificate does and does not establish¶

Value iteration can solve infinite-horizon reachability on a fixed learned WM/OM-induced graph. That is an infinite-horizon certificate for the learned model. It is not automatically an infinite-horizon guarantee for the real environment.

With approximate dynamics or opponent probabilities, persistent per-step model error accumulates. The paper's finite-H approximation bounds remain meaningful, but taking H -> infinity with a fixed nonzero error makes those bounds vacuous. A real-environment infinite-horizon theorem therefore needs exact stationary models, a separate simulation relation/robust uncertainty set, or an error/drift sequence with summable total mass. The exact true-policy shield is the clean diagnostic for separating model error from runtime shielding error.

Runtime movement of the OM posterior is another source of non-stationarity. The monotone floor and robust maximization over every remaining level are intended to make later level raises feasible, but they do not by themselves bound WM/OM approximation error outside the compiled level family.

Finite-horizon variants¶

For a deliberate H-step objective, use a distinct shield artifact and augment the safety state with remaining time:

V_0(s) = 1[Unsafe(s)]
V_h(s) = 1[Unsafe(s)] + 1[Safe(s)] min_a E[V_(h-1)(s')]

This computes the probability of hitting unsafe within h transitions. The time coordinate must be part of the shield state/certificate identity; a hidden episode cap cannot silently truncate a time-free graph. Because the WM/OM pipeline consumes the public state width, do not append graph-only time bits to the shared environment graph. Either expose time in the public environment state for an explicitly finite-horizon experiment, or build a separate shield-only dynamic-programming product whose cache metadata clearly records finite_horizon=H.

Finite-horizon runs are useful as diagnostics and for environments whose task definition is genuinely deadline-based. They should be labelled as finite and must not replace all main infinite-horizon runs.

Reset semantics¶

The current contract resets the safety budget and the reachability query at each env.reset(). It does not add an automatic reset transition to the infinite transition system.

That distinction is necessary. If independent episodes with positive failure probability are chained forever, the probability of at least one lifetime failure generally tends to one. Calling such a resettable process globally infinite-horizon safe would be misleading unless reset enters a formally specified regenerative objective (for example, per-cycle risk, long-run unsafe rate, or a lifetime risk budget that is allocated summably across cycles).

Use these labels in reports:

• model eventual risk/certificate: q and runtime action risk from the time-free infinite-horizon shield model;
• finite-window unsafe-episode rate: fraction of evaluated episodes with at least one observed unsafe state;
• unsafe-timestep rate/count: severity/persistence after entry, not the reachability objective;
• finite-horizon certificate: only for an explicit time-augmented H-step shield artifact.

The episode telemetry includes both reachability-oriented and severity metrics, and names the episode-window Brier score shield_finite_episode_reachability_brier to prevent it being mistaken for validation of an infinite-horizon guarantee.