A robot must deliver a parcel through a busy warehouse. Follow the same MDP from computing its safety values to carrying a risk allowance along a run.
There are eight decision states and two absorbing terminals. Collision is unsafe; Delivered is safe forever. The target is collision avoidance over an unbounded run, including any number of retries. A blocked route can keep you in the same state.
Click a state to inspect it. Faint arrows show possible safe-state routes. Coloured arrows show the selected action, labelled with its probabilities. β̄ is printed inside every state. Its collision arrow is red; absorbing terminal self-loops are omitted.
| Successor s′ | P(s′ | s,a) | β̄(s′) | P × β̄ |
|---|
This sum is the risk of taking this action once, then using a certified backup. It is different from its immediate collision probability.
| State | Action | Reward | Successor probabilities | Backup risk ρ |
|---|
Original teaching MDP, with explicit chosen probabilities and action rewards. It is not a warehouse environment from either paper. All displayed values are computed from these rows. Reward is an immediate progress score and does not enter the safety solve.
At an unsafe state the answer is 1. At Delivered it is 0. Elsewhere, try each action, average its successor safety values using its transition probabilities, and take the smallest result. Loops make the values depend on themselves.
β* is the least fixed point. An inductive upper certificate β̄ certifies a backup action at every state; ε describes its approximation error. Edwin writes βM for the optimum and β for the certificate; here we distinguish them as β* and β̄.
Delivered has value 0 and Collision has value 1. Slow exit reaches them with probabilities 0.94 and 0.02, and retries with probability 0.04. Sprint has collision probability 0.15.
The eventual risk is a little larger than the immediate 2% collision chance because a retry exposes the robot to risk again. This calculation uses the nominal fixed MDP, not the other model-selector settings.
| State | Lower Ln | Upper Un | Gap | Converged β̄ | Backup action |
|---|
A lower estimate only tells you that risk is at least that large. A shield needs a safe upper estimate. Iterate both, preserving L ≤ β* ≤ U, and stop when the largest gap is small enough. A small change between successive lower estimates alone does not certify the error.
Anchor unsafe states at 1 and the almost-sure safe set at 0. Here η = 10−12 is the outward numerical padding. This JavaScript example mirrors that update; it is not a call into the Python solver. For these small known rows, the converged gap is below 10−9.
Anchoring safe closed components matters. A safe self-loop would otherwise keep its initial upper value 1 forever. In this example only Delivered is almost-sure safe. See the repo solver, or use the one-loop intuition panel to isolate this issue.
Naming detail in the repo: SoundVIResult.q and
q_of(s) store the computed state upper bounds, corresponding
to β̄ here. The runtime q in (s,q) is the carried allowance, a different
quantity.
Choose an initial bound p. The shield starts at (Entry, p). At each step it checks an action and allocates a separate continuation allowance W(s′) to every possible outcome. After an outcome occurs, that branch’s allowance becomes the next q.
Edwin calls the successor-allocation function α and the action distribution v. Here W = α. A pure action is the special case va = 1. OmSh also uses α for an opponent posterior; that is a different object. Edwin encodes vertices of the feasible distribution polytope; the inequality also describes its convex hull. This panel restricts choices to feasible pure actions, preserving safety but potentially losing reward optimality.
Choose an outcome to examine its branch. These buttons do not change the transition probabilities. “Sample outcome” draws from the first retained kernel; in a robust model every retained kernel must satisfy the allocation constraint.
| Step | Before (s,q) | Action | max E[W] | Outcome probability | After (s′,q′) |
|---|
For one more step, the chance of eventually colliding on each branch is bounded by W(s′). Averaging over the next state gives at most q. Repeat this argument for any finite number of future steps, then take the limit. This requires valid kernels and a certificate at every step.
Simply allowing every action with a one-step collision chance below p would miss the accumulation across retries. Conversely, requiring every successor W(s′) ≤ q would unnecessarily forbid useful allocations to rare branches.
The initial p is chosen by the user. The backup certificate β̄ is computed. What PPO can learn is an action and an allocation W that preserves the safety inequalities. More budget at a successor can unlock a higher-reward action there.
The logits z are unconstrained learner outputs. Sigmoid σ creates a proposal between β̄ and 1. Radial projection scales its extra allowance until every retained level fits q.
| Successor | P · first kernel | β̄ | Raw W̃ | Executed W | Actions unlocked |
|---|
The grid search scores the expected next-step reward available after allocating W, averaged over retained kernels. It is a small transparent teaching objective, not PPO training or a global optimum. The sliders use this MDP’s actual successor action menus.
In the repo, PPO optimises return from trajectories in the augmented environment. The raw augmented action is scored by PPO; the projection executes inside the environment. It does not need a gradient through the projection. The intuition panel also covers pure actions versus learned pairwise mixtures.
An oncoming vehicle can yield or push forward. The joint-action world model Γ provides a transition row for each of those choices. Opponent level 0 yields with probability 0.2; level 1 yields with probability 0.8. These are chosen example policies, not a general meaning of reasoning levels.
Average over the opponent’s possible actions to obtain one MDP kernel for each imagined level.
| Successor | Γ · yield | Γ · push | P′₀ = .2 Γy + .8 Γp | P′₁ = .8 Γy + .2 Γp |
|---|
Choose one action first, then protect against every retained level at every step. This min–max is different from solving each level separately and taking the largest result.
| State | β̄ · floor 0 | β̄ · floor 1 | β̄ · mixture |
|---|
The safety-model selector above recomputes the whole example with the chosen floor. Removing a level can lower the backup demand; it does not refill q. The 50/50 mixture protects an averaged kernel and can miss the worst retained level. Use Levels & floors to compare the MAP, credible-tail, all-levels and mixture rules, and step through the patience gate.
Raising a floor is an assumption about which opponent models remain possible. It does not establish that the real opponent must now be cooperative. The robust guarantee requires the active kernel to remain inside the retained set.
~/Projects/quartz/omsh-paper/main.tex,
definitions augmented_sg, robust_floor_value,
runtime_replacement.
A winning-region shield asks: “Can I stay safe for sure?” A probabilistic shield asks: “Can I keep the chance of ever becoming unsafe within this run’s allowance?”
Allow actions whose eventual risk fits q.
At zero budget, an action must keep its entire probability support in states from which zero-risk continuation is possible. A bridge with even a tiny chance of falling fails that test. In deterministic dynamics, this recovers the familiar winning-region idea.
With q = 10%, an 8% bridge can be allowed. This toy has only one transition, so immediate and eventual failure coincide. In a longer game, they usually differ.
Edwin Hamel-De le Court, Belardinelli and Goodall augment the state with a risk allowance. Their encoded action chooses an action distribution and successor allowances, constrained by an inductive safety certificate. Paper, §3 ↗
OmSh’s default uses pure actions and an automatic allocation. Its optional parameterized modes also learn successor allocations and two-action mixtures.
A shield certifies a safe continuation, not just a harmless next move.
Before acting, assign an allowance to every possible next state. Keep their probability-weighted average within today’s budget. After the transition, carry the allowance of the state you actually reached.
Choose a realized successor to see the update:
Because the 60% allowance applies only after a branch reached with probability 20%. With A at 10% and B at 60%, the weighted allowance is 0.8 × 0.10 + 0.2 × 0.60 = 0.20.
This bounds failure from the original state by 20%, even if failure conditional on B can be as high as 60%. The budget can rise along a realized path; it is constrained in expectation.
The certificate β says how much eventual risk a safe backup may need. Assigning B a zero budget would leave no feasible continuation when its best available action still has 10% risk.
The default fill starts at β and raises all unsaturated allowances by the same amount until a constraint binds. Here it gives A = 19% and B = 24%. “Egalitarian” refers to equal increments.
Take a fresh 10% failure gamble each step. Each decision passes a naïve 10% check, but the chance of at least one failure grows.
With a global 10% budget and a first gamble that already has 10% immediate failure, the unsafe branch gets W = 1. The surviving branch must get W = 0, since 0.10 × 1 + 0.90 × W ≤ 0.10. You cannot take a second 10% gamble there.
Unsafe successors have certificate and allowance 1. Safe successors inherit a certified allowance. If their future failure chances stay below those allowances, the law of total probability bounds today’s failure chance by the weighted allowance, hence by q. Repeat this argument for any finite number of steps, then take the limit. Robust OmSh enforces the same inequality for every retained opponent level, using one shared W vector.
The next budget is selected by the outcome. It is not “q minus the action’s risk.”
Value iteration propagates risk backward through the graph. The repo tracks a lower and an upper bound on the minimum eventual failure probability. The shield uses the upper bound.
You may revisit the room many times. Solve V = 0.02 + 0.92 V to get V = 0.25. A small immediate hazard can hide a large eventual risk.
Start with L = 0 and U = 1. L rises and U falls. Their gap measures remaining uncertainty about the solution. Small changes in L alone do not certify a small error.
An upper bound may block an action before enough iterations have tightened it. That is conservative: it avoids admitting an action using an optimistic estimate.
An inductive certificate also satisfies Bellman(β) ≤ β. That means every state has a backup action whose expected successor certificate fits its own certificate. This gives the budget a feasible continuation.
If a room loops to itself safely with probability 1, its true minimum failure probability is zero. But starting at U = 1 gives Unext = U forever.
A small residual (zero!) did not find the right value.
The repo first finds the largest safe set with an action that keeps all supported outcomes inside it and has no missing mass. Those states are fixed to zero. Unsafe states are fixed to one. Unaccounted probability goes to an explicit unsafe sink, rather than being renormalized away.
The paper permits several algorithms producing an inductive upper
certificate, including Sound Value Iteration. The repo’s function
named sound_value_iteration_min_reach_upper uses
monotone lower/upper interval updates, an almost-sure safe-set
anchor, and outward numerical padding. This toy illustrates that
implementation’s nominal interval logic; it does not reproduce every
step of the published Quatmann–Katoen algorithm.
With optional transition ambiguity sets, the lower and upper operators can have different fixed points. Their gap can then express model uncertainty as well as numerical error, so it need not close to zero.
VI computes a backup risk certificate. PPO later learns reward-seeking behaviour inside its constraints.
The learner cannot vote to ignore max_risk. It can
discover that extra allowance is more valuable in one future state
than another, and propose a better allocation.
The experiment’s safety target. Raising it changes the contract.
A conservative backup demand, computed from the WM/OM graph.
How to distribute allowance to improve future return.
A finite grid search illustrates the objective. This website does not train PPO.
The raw Gaussian action gives logits z. Convert each to a proposed allowance between β and 1 using a sigmoid. If the proposal overspends, shrink all its extra allowances by the same factor λ until every active level’s constraint holds.
This preserves the learner’s allocation direction. It is a radial projection from β, rather than the nearest point in Euclidean distance.
Higher WB can unlock B’s high-reward action. If B is reached, the policy observes that budget and uses the opportunity. PPO connects the later return to the earlier proposal.
PPO stores and scores the raw augmented action. The shield’s sigmoid, projections and primitive-action sampling are environment dynamics. Learning does not need to backpropagate through the shield.
Skip zero denominators. An infeasible β means the state’s backup needs more risk than q: raise an infeasibility error. Numerical projection failures fall back to β. Safety is a hard constraint; a high reward never compensates for overspending.
| Variant | Primitive action | Successor allocation | Config value |
|---|---|---|---|
| Egalitarian Pure DEFAULT | One action | Automatic equal increments | pure |
| Egalitarian Mixed | Learned two-action mixture | Automatic equal increments | egalitarian_mixed |
| LearnedBudget Pure | One action | Learned, then projected | learned_budget_pure |
| LearnedBudget Mixed | Learned two-action mixture | Learned, then projected | learned_budget_mixed |
For actions A and B, L0 gives risks (10%,50%) and L1 gives (50%,10%). At q = 32%, neither pure endpoint is safe against both levels. An intermediate mixture can be.
Both level constraints must hold. Sampling B need not be individually admissible as a pure action at q. A third backup action has 25% risk under both levels.
The combined variant first projects the action mixture using β, then projects W using that mixture’s successor probabilities. Pairwise mixtures do not represent every possible distribution over three or more actions. PPO may also find a poor allocation; projection guarantees feasibility, not optimal learning.
“Learn the budget” means learn its allocation while the shield enforces the chosen limit.
Opponent levels are imagined policies, not danger scores. The posterior measures which level explains observed behaviour. The floor says which lower-level hypotheses the shield has permanently removed.
The opponent’s behaviour may change. An inferred level does not make the real opponent change.
Soft weights over L0, L1, L2. These can move up or down after observations.
At f = 1, safety is robust over L1 and L2. L0 has been excluded.
| Action | L0 | L1 | L2 | Used risk | Admissible? |
|---|
Toy risks are eventual terminal-failure probabilities. “Wait” gets more dangerous at higher levels; “Shortcut” gets less dangerous.
INJECT ONE NEW POSTERIOR
Each button stands for one successful opponent-model update. These weights are illustrative inputs, not a fitted Bayesian model.
Changing mode or patience starts a new toy instance. Episode reset preserves posterior, floor, streak and observation count.
| Update | Posterior (L0 / L1 / L2) | Estimate | Streak | Floor |
|---|
L0 copies opponent behaviour from pre-training. To imagine L1, first train a focal response to L0, then an opponent best response to that focal policy. Repeat the alternating responses to build L2. Intuitively: “I adapt to you adapting to me.” These are offline imagined policies, not three observed stages the real opponent is guaranteed to pass through.
The online OM asks which of those policies best explains each observed opponent action. Its Bayes-style likelihood update is temperature-smoothed and averaged over time. That belief update is separate from the shield’s patience gate. None of these steps implies that higher levels are more dangerous: compare Shortcut and Wait in the toy table.
The default uses the most likely level (MAP) as the estimate. A 40% lead can request a raise even with 60% belief elsewhere. Patience counts consecutive successful updates supporting the next raise; contradictory evidence resets that streak.
With patience 3, a jump in the estimate to L2 takes three supporting updates to reach floor 1, then another three to reach floor 2. With patience 0, the implementation jumps directly to the estimated level. Calling inspection repeatedly does not count as new evidence.
Choose the largest suffix whose posterior mass is at least 1 − δt, then apply the same patience gate. A weak L2 lead usually leaves L0 in the set.
The floor remains irreversible even if the posterior later reverses. The repo logs excluded mass and a tail-constraint miss; it does not lower the floor or repair the assumption automatically.
| Mode | Safety aggregation | What the claim needs |
|---|---|---|
monotone_floor |
Worst case over ℓ ≥ f | True active level remains in that suffix; patience alone does not prove this. |
credible_floor |
Worst case over a credible suffix | Calibrated posterior coverage, monotone true levels, correct/covered dynamics. |
all_levels |
Worst case over every level forever | True transitions remain in the compiled level family, even when levels switch downward. |
bayesian_mixture |
Posterior-weighted transition | A model-relative mixture interpretation; no worst-case level-switching claim. |
The summable schedule spends δt = 6δ / [π²(t+1)²]. All its allowances together sum to δ. A union bound can then control “ever excluded the true level,” under the stated calibration and monotonicity assumptions.
These are union-bound allowances, not measured exclusion rates.
For credible-floor notebook runs, a total target of 20% with a 5% tail
allowance initializes the model-controlled budget at 15%. With the
summable schedule and the required assumptions, the nominal total is
15% + 5% = 20%. Direct wrapper construction takes the model component
as init_safety_bound. A fixed schedule does not give this
anytime tail guarantee. Credible-floor is retained as a
diagnostic/ablation; the current primary comparison uses
monotone-floor.
The robust certificate solves a minimum over actions, followed by a maximum over retained levels. Removing levels weakens that maximum, so the required backup risk cannot increase. A successor budget assigned under the old floor still covers the next state after a raise. The floor change itself does not alter q.
Bayesian-mixture mode keeps an all-level robust continuation certificate but uses the current posterior mixture for the one-step action and allocation constraint. This preserves a feasible backup after posterior changes; it does not establish a full belief-state infinite-horizon theorem.
Higher levels are different policies. A higher floor removes hypotheses; it does not make the world inherently safer.
World modelling gives the transition probabilities. Opponent modelling gives the level-specific policies. The shield combines them, computes a backup certificate, and carries a budget while the reward policy learns.
Pℓ(s′ | s,a) =
Σopponent actions Γ(s′ |
s,a,a−i) π̃ℓ(a−i | s)
mina maxℓ ≥ f
Eℓ[β̄f(s′)]
≤ β̄f(s)
Check against q.
Project W.
Carry W(realized s′).
Suppose A has risk 0 under L0 and 1 under L1, while B has risk 1 under L0 and 0 under L1. Each level separately has minimum risk 0, but no single pure action achieves that across both levels. The robust pure-action value is mina maxℓ risk = 1, whereas maxℓ mina risk = 0.
The repo therefore computes a separate robust floor-wise continuation certificate rather than taking the maximum of independently solved level values. Optional mixed variants also retain this conservative pure-action certificate as a lower limit on successor allowances. They can improve current-step choices without solving an optimal mixed-action continuation program.
The default graph is time-free and targets eventual unsafe reachability. A hidden simulator step limit does not silently turn this into a finite-horizon certificate.
Reset starts a new episode’s risk query and restores its initial budget. A per-episode 10% bound does not mean at most a 10% chance of ever failing across infinitely many episodes.
A sound solve certifies the supplied model. Real-world safety additionally depends on dynamics accuracy, graph support and coverage, unsafe labels, and the actual opponent staying within the retained assumptions.
Missing mass is treated as unsafe. This handles explicit graph deficits; it does not automatically bound all errors in learned probabilities.
Learned OmSh: freezes a bundle induced from learned world/opponent models. Its certificate is relative to those kernels unless further error guarantees apply.
True-policy shield: uses exact dynamics and the current live opponent policies, periodically rebuilding the bundle. Exact policy access is an evaluation baseline, not a guarantee against arbitrary opponent actions.
Exact anytime adversarial audit: preserves each joint-opponent-action row and takes its worst case. An independently checked certificate can bound one focal agent’s per-episode risk against arbitrary opponent actions on the declared exact graph and reset support. It may be infeasible at the chosen target; it is separate from the default learned floor heuristic.
Optional count-based ambiguity sets and padded transition constraints address probability uncertainty under their own support, confidence and coverage assumptions. They do not learn the initial risk target. See the source notes below for the theorem-facing details.
| Symbol / setting | Meaning here | What changes it? |
|---|---|---|
max_risk |
Chosen initial episode target | Experiment configuration |
q / current_safety_bound |
Current conditional risk allowance | Realized successor’s W, or episode reset |
| βf | Robust backup certificate for floor f | Offline bundle build / selected floor |
| W(s′) | Allowance assigned to a possible successor | Egalitarian fill or projected learned proposal |
α / mix_alpha |
Opponent-level posterior weights | Observed opponent actions and OM update |
f / level_floor |
Lowest retained opponent level | Configured estimate rule and patience gate |
| δtail | Allowance for credible-level exclusion | Configuration and schedule, not PPO |
Checked against the local repo and
~/Projects/quartz/omsh-paper on 2 October 2026. Every
numerical demo is a toy, not an experiment result.
PPO learns actions and allocations; the shield checks their continuation-risk constraints.
The world model predicts what happens after joint actions. The opponent model predicts which actions the other agents take. Together they give the transition rows used by the shield.
Level 0 clones observed opponent behaviour. To construct level m + 1, improve a focal policy against opponent level m, then improve the opponent against that focal policy using imagined rollouts. This is an alternating best-response construction, not a measurement of an opponent’s intelligence.
Fit the next policy to this soft target. The rollout horizon H helps build the opponent hypothesis; the shield’s unsafe-reachability objective remains infinite-horizon. The method needs observed or derivable opponent rewards.
Exact Bayes is T = 1, η = 1. The implementation can temper and smooth the update. These α values are beliefs over levels; Edwin’s allocation α is the W used elsewhere on this site.
Use the warehouse’s two hypotheses: level 0 yields with probability 0.2, level 1 with probability 0.8. Begin with equal prior weight, then observe yield or push.
| Observation | Prior α₀ / α₁ | Exact Bayes b₀ / b₁ | Tempered, smoothed α₀ / α₁ |
|---|
This demonstration applies the stated Bayes/temperature/EMA equations to fixed hypotheses. It does not train opponent networks or advance a floor. Raising the floor is a separate irreversible decision, illustrated in Levels & floors.
The posterior can rank already-safe actions by expected reward. Robust safety still checks every retained level, using one common W. A high posterior weight does not turn a model prediction into a coverage guarantee. Higher levels also need not be safer; the warehouse’s more cooperative higher level is a chosen example.
~/Projects/quartz/omsh-paper/main.tex, sections
Multi-agent Model-Based Opponent Modelling and Probabilistic
Shielding.Belief update implementationImagined-level construction
A valid certificate gives a bound for the dynamics it covers. Your manuscript explains how to lift that statement to the real game, including model uncertainty and opponents that change over time.
The equations below show the pure-action special case. The updated manuscript also permits a distribution over action–allocation pairs and outer sets of whole action-row families: see Randomisation & timing. Count-based coverage makes the statistical set concrete; Risk dominance gives a weaker sufficient condition.
The set and allocation must be chosen before seeing the next outcome, with a feasible certificate at every safe history. The theorem starts at a safe initial state and does not cover an uncertified pre-training prefix.
Before a collision or the first coverage failure, the average next allowance is at most the current one. In probability language, this is a nonnegative supermartingale. Freeze it at either event: entering Collision forces q = 1, so the probability of a covered collision is at most the initial p. Coverage can fail with probability at most δcov; add that once. Conditioning directly on “coverage holds forever” could change transition probabilities, so the manuscript uses this stopped-process argument.
These bounds concern one focal agent and one run carrying its budget. Restoring q = p at reset starts a new per-episode query; it does not create a single lifetime bound across repeated resets.
Checking all retained rows also checks their convex combinations. This tolerates arbitrary switching among covered levels. Raising the floor reduces the checked set and can loosen β̄, provided the computed certificate family is ordered accordingly. It leaves the carried q unchanged. Safety under this coverage theorem still requires the true row to remain covered: a MAP estimate alone does not establish that, and an irreversible floor can exclude a model that later fits the opponent again. Failure of coverage alone does not prove a safety failure; the updated risk-dominance corollary examines the committed W directly.
| Quantity | What it means | Where it enters |
|---|---|---|
| εVI | Error in the computed β̄ relative to β*. | Conservatism of the safety certificate; not an extra failure probability when β̄ is valid. |
| r = εWM + εOM | TV-distance radius around induced level kernels. | The robust next-state set. A radius needs a valid coverage argument. |
| δcov, optionally δtail | Probability that the coverage contract fails, or a separately justified credible-floor exclusion fails. | Reserve these from the end-to-end risk target; avoid counting the same event twice. |
A small persistent point-model error is insufficient for infinite-horizon safety. If a model says “safe self-loop” but the real process has an unmodelled collision probability ε on every visit, its risk after H visits is 1 − (1 − ε)H, tending to 1. The true law needs to lie in the set the shield actually checks.
Assume the displayed error probabilities have been justified. For a separately accounted credible-floor tail, use p = ptotal − δcov − δtail. If δcov already covers all floor exclusions, set the additional tail reserve to zero. A summable tail schedule is conditional on the stated calibration and level assumptions.
The feasibility comparison uses the warehouse’s floor-0 certificate, β̄(Entry) ≈ 17.68%. These sliders illustrate accounting; they do not certify model coverage. Enlarging a real ambiguity set also requires recomputing its backup demand.
Edwin’s full construction includes the feasible action-distribution polytope’s vertices and arbitrary valid successor allocations. With the exact safety value it recovers the optimal safe reward under the paper’s assumptions; the approximation-limit result uses strict feasibility (Slater’s condition). Our pure-action trajectories and restricted allocation search preserve the safety inequalities but can remove reward-optimal choices. PPO itself is not guaranteed to find a global optimum. OmSh adds conservatism over opponent levels and model uncertainty.
Your updated robust permissiveness theorem states a path-law approximation bound for the full randomised shield at a fixed level set. It separates the mixed robust value from the pure certificate and does not claim that the implemented PPO controller finds the existential policy.
The slides use βt for the carried budget, corresponding to qt here; their β* is the minimal risk, and α is the successor allocation W. Their δ for VI termination is an accuracy tolerance, not δcov.
Printed slides 103 and 109 put βt+1 on the right of the expected-allocation inequality. Under the stated state/action timing, this appears to be an indexing typo: Edwin’s Definition 3 compares the allocation to the current budget qt, then sets qt+1 from the realised successor. This website follows Definition 3.
as:anytime_coverage,
def:anytime_runtime_certificate,
thm:anytime_safety, cor:padded_omsh and their
appendix proofs.
Your paper now distinguishes the pure-action runtime wrapper from a more permissive randomised shield. The key question: can the opponent see your sampled action before choosing its level?
The opponent may use the entire past to pick today’s level. It picks before the focal controller draws today’s action and allocation. It knows the distribution, but cannot react to the draw.
For a general outer family set, replace max over levels with sup over F ∈ 𝔉, and P′ℓ(· | s,a) with Fa. One F describes the rows across all sampled actions together.
For this calculation, a crossing ends in Delivered or Collision; W is 0 or 1 respectively, so the table entries are both collision probabilities and expected successor allowances. The ten-state warehouse remains the multi-step example.
| Chosen level | Action A | Action B |
|---|---|---|
| L0 | 0% | 40% |
| L1 | 40% | 0% |
Let x be the probability of B. A single level produces risk 40%x or 40%(1 − x). With x = ½, both give 20%, even though each pure action’s worst case is 40%.
| Level held for the draw | Mixture’s E[W] | Budget check |
|---|
If the opponent could react after seeing A or B, it could always pick the dangerous level. Then E[maxℓ cost] is 40%, whereas maxℓ E[cost] is 20% at the balanced mixture. Neither calculation averages levels using posterior weights.
At q = 20%, this crossing can use its exact mixed certificate: β(Entry) = 20%, β(Delivered) = 0 and β(Collision) = 1. Keeping the 40% pure certificate would fail the theorem’s initial β(s₀) ≤ p premise at that budget. The next page explains this certificate gap.
β is an inductive certificate with β = 1 on unsafe states; hence every sampled W also equals 1 there.
The draw can choose A with WA, or B with WB. An individual pair need not fit q by itself: the distribution must fit every level’s expectation. After the draw, use that pair’s W. Replacing this constraint with a check of every sampled pair would discard safe mixtures.
The existing pairwise learner uses a common W and a selected action edge; the pure runtime wrapper uses a point mass on one (a,W). Both are restricted constructions. The theorem describes the larger set, rather than claiming those implementations explore all of it.
For finitely supported ν, the paper’s “Few atoms suffice” proposition decomposes it into feasible mixtures, each using at most |Λ| + 1 pairs from its support. Three retained levels mean at most four pairs per component. Preserving an arbitrary original path law may require randomising over those components; the proposition does not compress every distribution into one four-pair distribution.
Source: omsh-paper/main.tex, def:fixed_floor_shield,
thm:fixed_floor_permissive, prop:two_atoms. The timing is part of the
mathematical model, not a switch to change the opponent’s information in the
deployed game.
Soundness says every admitted controller is safe. Permissiveness asks whether safe policies can still be represented. Your updated theorem quantifies that second question.
Both operators fix unsafe states to 1; the displayed minimisations apply at safe states. Here β is an inductive certificate, with β = 1 on unsafe states and TmixΛβ ≤ β. A pure-action upper certificate is also valid for the mixed operator and additionally lies above β*Λ. It may be conservative even if its pure-action solve is exact. In the previous page’s crossing, the pure value is 40% and the mixed value is 20%.
Fix a nonempty level set Λ and any history-dependent policy π that is p-safe against every allowed level sequence. There exists a compliant, potentially history-dependent controller with this approximation guarantee under every sequence. It is an existence theorem; it does not say PPO finds that controller.
Intuitively, inflate π’s continuation allowances to clear the upper certificate, then put a little probability on an inductively safe backup. The backup compensates for the inflated initial expectation. More initial slack means less backup mixing is needed.
This calculator assumes a valid β with β(s₀) = 15% and the supplied global gap d. It does not construct such a certificate. d is an absolute probability difference, not a percentage of β. For discounted rewards bounded by |r| ≤ R and γ < 1, one can take B = R/(1 − γ).
Start mixed Bellman iteration from 1U to obtain a lower iterate βk. Then βk ≤ βmixΛ ≤ β and d ≤ ‖β − βk‖∞. Substituting that upper bound for d gives a conservative ε bound. Each mixed update solves a small matrix game; the website’s original warehouse solver still uses the pure operator.
Source: omsh-paper/main.tex, thm:fixed_floor_permissive and its
proof; campaign values checked at revision e049b7c. Original-game reward
optimality still depends on whether the level model excludes policies that
the real opponents make safe.
The learned world model is useful for imagination and reward prediction. The paper’s concrete statistical certificate is centred on observed transition counts. They have different jobs.
Fix one state–joint-action row with m legal successors. After n visits, P̂n is its empirical distribution. Choose a total coverage-failure budget δcov, divide it across the finite set of R rows, and spend each row’s allowance across all visit counts.
For m > 1, use a uniform centre and radius 1 at n = 0. For m = 1, the radius is 0 even without visits, because a correct singleton support already determines the row. Adaptive visit times are allowed under stationary, state-sufficient dynamics with fresh transition randomness. Changes in the environment’s transition law would require another argument.
δcov is chosen by the designer, not learned from held-out accuracy. The data determine the centre and radius. The statement is simultaneous over all counts and all rows, so it pays miscoverage once.
Here one legal row has three successors and W = (5%, 30%, 100%). For positive n, counts keep the proportions (60%, 35%, 5%) to isolate the effect of sample size. Increasing n here is a comparison of count tables, not simulated new observations. Marked route and Inspection retain those continuation allowances; Collision has W = 1.
| Legal successor | Committed W | Empirical P̂ | Worst-case P |
|---|
The exact supremum moves up to r probability mass from low-W successors to high-W successors. Donors can run out and recipients can fill up, so the displayed cheap bound is an inequality.
A count-derived radius cannot simply be placed around the learned Γ. By the triangle inequality, radius min{1, rn + TV(P̂n,Γ)} around Γ contains the count ball and retains its coverage, but may be wider. The paper keeps the count-centred set as the certified object.
Joint-action row coverage must then be combined with an opponent-action envelope. Taking all opponent distributions covers arbitrary adaptive behaviour; a narrower envelope needs its own validity argument. Complete legal support and correct unsafe labels remain necessary. An ambiguity ball redistributes legal mass; it does not invent an unsafe successor that the dynamics rule out.
After a data-collection prefix, freeze these sets. With probability at least 1 − δcov over that prefix, every later compliant episode is p-safe, conditional on the prefix, provided the opponent envelope always covers its behaviour. This is a two-stage statement, not a bound on ever failing across infinitely many episodes. The uncertified collection prefix is outside it.
For the unconditional one-run target ptot, the earlier accounting still uses p = ptot − δcov. Neither count-based coverage nor padded level sets remove the need for a feasible runtime certificate at every safe history.
Source: omsh-paper/main.tex, prop:tv_confidence_sequence,
cor:row_union_bound, lem:tv_ball_bellman, cor:frozen_sets. This row
calculator is ordinary floating-point teaching code, not a certified
whole-game solver.
For the pure runtime wrapper, coverage contains the true law in a certified set. Risk dominance asks something weaker: under the W actually committed, does the true expectation still fit the carried q?
W is chosen before the next outcome, stays in [0,1], and equals 1 on unsafe successors; q′ = W(s′). The excess-corrected stopped budget is a supermartingale. An outside-set opponent can have zero excess if it avoids transitions with large W.
This corollary measures excess after (a,W) is drawn. A general randomised shield can be safe in expectation over ν even when some sampled pairs have positive excess. Thus zero excess for each realised pair is not required by the randomised soundness theorem. Here we analyse the pure per-step wrapper and its committed W.
Collapse a warehouse run to Entry, Inspection, Delivered and Collision. Entry and Inspection use the same row; Inspection can repeat, and the other two destinations are absorbing. Start at Entry with p = 30%. Commit W(Delivered) = 0, W(Inspection) = 40%, W(Collision) = 100%. Entering Inspection therefore carries q = 40%; it does not refill to 30%.
The certified row centre is (50%, 40%, 10%), with TV radius 2% on these three legal successors. Its worst expected W is 28%, fitting both Entry’s 30% and Inspection’s 40%. Below, choose the true row and compare coverage with excess.
| Successor | True probability | Carried W |
|---|
Write w for Inspection probability and c for Collision probability. Collision by T has probability c∑t=0T−1wt. Entry’s excess is (c + 0.4w − 0.3)+; Inspection’s is (c + 0.4w − 0.4)+. The expected stopped excess sum is ηEntry + ηInspection∑t=1T−1wt. Delivered contributes no future excess. We compute these expectations exactly for this fixed toy row, rather than multiply an observed step excess by a horizon.
With a known true kernel, the calculator can evaluate the true expectations. Without it, sample episodes can estimate them. Zero excess on sampled steps does not establish zero excess almost surely, and a plug-in average is not a certified expectation bound.
| Current manuscript audit | Deployed p | Worst-seed plug-in p + mean stopped excess |
|---|---|---|
| Congestion (both roles) | 0.10 | 0.10 |
| Bertrand, Chicken, Markov Stag Hunt | 0.20 | 0.20 |
| Gathering | 0.20 | 0.2002 |
| Pursuit–Evasion | 0.16 | 0.291 |
Snapshot of figures/tables/dominance_audit.tex at e049b7c:
frozen-policy evaluation, 200 episodes per seed, five seeds. These are
reported empirical estimates. The paper counts excess below 10⁻¹² as
floating-point noise; the toy calculation above uses the mathematical
positive part.
A floor rising past the closest level can break the coverage argument. It does not logically imply a safety failure: the actual law may still satisfy risk dominance. Conversely, the floor heuristic does not prove either condition. The paper’s patience screen delays raises with patience 4096, but retains patience 64 as primary because the larger value does not improve reward consistently across environments.
Use coverage for a prospective safety certificate. Use the dominance audit to investigate whether a learned shield’s committed W was risk-conservative in the evaluated trajectories. The original anytime theorem still allows non-monotone opponent behaviour whenever the actual family remains covered.
Source: omsh-paper/main.tex, cor:risk_dominance,
appsec:dominance_audit, and “The monotone floor in practice”;
figures/tables/patience_screen.tex. The trained-policy audit
covers frozen evaluation, not the changing opponents during training.