Interactive probabilistic-shielding field guide¶

Created 2026-10-02 for a reader familiar with deterministic winning-region shielding, but unfamiliar with state-augmented risk accounting and opponent floors. A versioned snapshot lives in teaching-site/; the requested deployment at ~/Documents/omsh-website is also a standalone Git checkout, hosted privately at nightly/omsh-website. The independent repository owns its .gitignore and README.md. Website changes are not automatically synchronized back to this OmSh snapshot; do not overwrite its uncommitted changes when refreshing static files.

Implementation¶

The site is plain HTML, CSS, JavaScript and inline SVG, with no remote runtime dependencies. index.template.html holds the lesson markup. The dependency-free Node script build.mjs embeds the CSS, JavaScript and favicon into the shipped index.html, so opening the website needs no build step and no sibling files. Scripts execute at the end of the body, after their controls exist. Hash navigation shows the worked MDP or one of six intuition lessons, retains toy state when moving between lessons. Two further theory pages cover opponent model construction and original-game guarantees. Four updated-manuscript chapters add simultaneous-move randomisation, robust permissiveness, count-centred coverage and risk dominance. There are thirteen chapters in total. Navigation supports browser back/forward, and moves keyboard focus to the main region. Without JavaScript, the explanatory text is visible for all lessons. Printing exposes all lessons. CSS supports narrow screens and reduced motion. Source links point to the repository on GitHub; local content does not require network access.

shield-math.js is the small pure calculation layer, shared by the browser and the Node verification script. It is not imported by production shielding. app.js owns only inputs, presentation, lesson navigation and toy history. The website makes no changes to runtime shielding, training, or experiments.

Ten-state worked MDP¶

The opening panel now teaches one fully specified warehouse MDP rather than asking readers to infer multi-step behaviour from the smaller terminal toys. It is separate from the six intuition lessons. Its five tabs cover the model, the safety solve, a carried-budget run, allocation learning and opponent levels. A restrained notebook layout replaces the decorative landing page.

mdp-section.html owns equations and controls; mdp-model.js owns the rows, safe-set calculation and interval solve; mdp-app.js owns the graph and interactions. worked-mdp.css styles this panel and simplifies the shared typography. build.mjs embeds all of them into the single shipped HTML. Opening the website still requires neither a backend nor sibling assets.

There are eight transient decision states with two actions each and two absorbing terminals, Delivered and Collision: ten states, eighteen state-action rows. Several actions have self-loops; paths rejoin at Inspection and Exit lane. The probability rows and action rewards are authored teaching data, not a warehouse environment from either paper or an experiment result. The nominal optimal reset risk is approximately 0.1467046039. The example starts with allowance p=0.25. Reward never enters the safety Bellman solve.

The notation distinguishes the exact least fixed point beta* from its computed inductive upper certificate beta-bar. Runtime uses the converged upper certificate, not the currently selected VI iteration. The interval solver mirrors the nominal Python update with 1e-12 outward padding, unsafe states anchored at one and almost-sure safe states anchored at zero. For these rows its converged interval gap is below 1e-9. The graph labels round to percentages; calculations retain full precision. This is a JavaScript teaching implementation, not a production solver call or a reproduction of the published Quatmann–Katoen algorithm.

The runtime tab admits pure actions using their expected successor certificate and applies the egalitarian allocator. Outcome buttons explicitly explore a branch without changing its probability; random sampling uses the first retained kernel. A two-step preset reaches North aisle, then takes its self-loop, showing distinct q values at the same physical state. The trace includes the previous augmented state, executed action, maximum certificate expectation, branch probability and resulting augmented state. Initial allowances below the reset demand are reported infeasible.

The learner tab applies the actual sigmoid proposal and radial projection formula to Entry's successor budgets. The alternative egalitarian allocator and a 25-proposal logit grid are compared using the expected next-step reward opportunity from this MDP's admissible successor action menus. At q=0.25, the marked route scores 1.0 under egalitarian allocation and 2.05 under a feasible searched proposal. This objective is explicitly a teaching surrogate, not PPO or a guarantee of optimal long-run allocation. The original learning lesson still covers the repo's pure/mixed action parameterizations and PPO.

The level tab derives two induced kernels by combining conditional world rows for opponent actions yield/push with opponent yield probabilities 0.2 and 0.8. Yield halves collision mass; push multiplies it by 1.4; the changed mass comes from the first forward successor. The nominal kernel corresponds to yield probability 4/9. Floor 0 checks both kernels; floor 1 retains only the higher level; the mixture ablation averages with weights 0.5/0.5. In this particular toy, the weaker level dominates collision risk for every action, so the robust solve equals its nominal solve. This is not a general property of reasoning levels or min_a max_level. At (Entry, q=0.20), Express is blocked at floor 0 and admitted at floor 1 without refilling q. Changing the global model selector intentionally resets the demonstration trajectory; the separate comparison explains the fixed-history floor change.

Equations are attributed to Edwin's §3, Definitions 2–3, and the current omsh-paper/main.tex labels def:augmented_sg, def:robust_floor_value and def:runtime_replacement, plus its successor-allocation paragraph. Edwin's allocation alpha is explicitly mapped to runtime W; OmSh's posterior alpha is a different object. The general (allocation, distribution) constraint is displayed. A naming note distinguishes SoundVIResult.q and q_of(s) (state certificates) from runtime q (history allowance), and a hand-solved Exit lane loop gives the nominal value 1/48. The worked trajectories use its pure-action special case. Higher-level guarantees remain conditional on the active kernel staying in the retained set. The floor lesson keeps the detailed MAP, credible suffix, patience, all-level and mixture mechanisms.

mdp-check.cjs, included by check.cjs, independently evaluates all 256 deterministic stationary policies per kernel via linear systems. It checks the interval against that reference, inductiveness, row normalization, projection feasibility, safe closed-component anchoring, antitone floors, history-dependent allowances and the reward comparison. Combined checks pass 26,080 assertions. browser-check.cjs passed Chromium and Firefox over isolated single-file loading and HTTP, seven widths (2879, 1440, 1366, 1024, 768, 390, 320), all worked tabs/model modes, old lessons, keyboard tab navigation and the no-JavaScript reading path. No page errors or horizontal page overflow were found; final desktop, phone, solve and allocation screenshots were visually reviewed.

open-website is an executable Bash launcher, copied with mode 755 into the local deployment. It resolves index.html relative to its own directory and opens it with the default desktop browser using xdg-open, with gio open as a fallback when xdg-open is absent. It works from other working directories and handles spaces in the website path. Direct file access requires no server, Python process, or port allocation. A missing index gives a readable error.

Desktop file-portal repair¶

The first desktop launch in Flatpak Firefox showed a huge blue shield instead of the layout. The screenshot's URL was under /run/user/1000/doc/.../index.html; the default Firefox desktop entry uses Flatpak --file-forwarding. Such a document-portal launch can expose only the selected HTML file, leaving the relative CSS and JavaScript unavailable. The early browser checks opened HTML with its siblings still present, so they did not cover this situation.

The failure was reproduced by copying the original index into an otherwise empty directory: the logo expanded to the viewport, default link blue replaced the theme, and ShieldMath was missing. The shipped HTML now embeds every rendering/runtime asset, including the favicon. The existing launcher therefore works without granting wider filesystem access or starting a server. A tiny Node build step was chosen over a background HTTP service because it fixes both direct HTML opening and the launcher, with no process lifecycle or port to maintain. Source HTML and generated HTML are separate; run node build.mjs after source edits and node build.mjs --check before committing.

Visual polish also aligns the header, progress, lesson and footer in one centered column and keeps navigation beside it on wide windows, prevents the brand subtitle wrapping, gives the SVG logo explicit fallback dimensions, and uses a more compact opening lesson on short desktop viewports. No shielding calculations changed.

Regression checks open only the generated HTML in an empty directory in both Chromium and Firefox, exercise every lesson, and assert that no sibling asset or network request is needed. The tested widths include the user's 2879-pixel screenshot, 2048, 1366, 1024, 390 and 320 pixels. check.cjs also rejects external stylesheet/script references in the shipped HTML.

Toy models and boundaries¶

Bridge: two terminal routes, a zero-risk detour and a configurable failure-probability shortcut. Immediate and eventual risk coincide only because both terminate. Setting budget zero connects support-based safety with the deterministic winning-region construction.
Branch budgets: one safe decision state leads to A/B with probabilities (0.8, 0.2). Their exact continuation floors are (0.05, 0.10), implemented conceptually as terminal-risk backup actions. At parent budget 0.20, (0.10, 0.60) is feasible and robust egalitarian fill gives (0.19, 0.24). Realizing B carries 0.60; it does not subtract a risk from 0.20.
Interval VI: one transient room loops with probability 0.92, exits safely with 0.06, and reaches unsafe with 0.02. Exact eventual risk is 0.25. Starting at [0,1], analytic bounds after n passes are L_n=0.25(1-0.92^n) and U_n=0.25+0.75*0.92^n. A separate safe self-loop explains why the zero-valued invariant set is anchored before iteration. Numerical outward padding is omitted in this analytic visualization.
Learned allocation: same branch floors; Gaussian-logit proposals use beta+(1-beta)*sigmoid(z) and the repo's radial projection formula. A second optional safety row (0.6,0.4) demonstrates intersecting constraints. State-specific menus attach reward to actions with terminal failure probabilities, so future feasible-set changes determine reward. The demonstration searches 625 proposals; it is explicitly not PPO training. The objective always uses branch weights (0.8,0.2), separately from safety.
Pairwise mixture: opposing terminal-risk rows (0.1,0.5) and (0.5,0.1). At budget 0.32, the feasible coordinate is [0.45,0.55]. A third pure backup has risk 0.25 under both levels and is used if the selected edge is empty. This avoids conflating safe mixtures with individually safe endpoints.
Floors: prescribed posterior observations illustrate MAP/credible estimates and positive-patience one-level gates; patience zero jumps directly to the estimate. Every injected posterior is exactly one successful update. This UI does not implement the actual OM's Bayes/temperature/EMA filter. Episode reset preserves posterior, floor, streak and continuing observation count; restarting the experiment clears them. Toy action rows terminate, allowing exact risk aggregation without a hidden continuation solve.

The interval demonstration explains the code's interval scheme; it does not claim to reproduce the published Quatmann–Katoen Sound Value Iteration algorithm. The main robust continuation certificate is pure-action min_a max_level; the optional mixed modes still use that conservative continuation certificate.

Source audit and interpretation¶

Primary local sources are src/shield/transition_shield.py, sound_value_iteration.py, inspection.py, augmented_action.py, parameterized_transition_shield.py, src/rl/parameterized_ippo.py, and notebooks/utils/shielding.py, plus the local omsh-paper/main.tex and runtime algorithm. The source snapshot began at commit 2b26df9.

External references are Edwin Hamel-De le Court, Francesco Belardinelli and Alexander W. Goodall's AAAI 2025 paper and Quatmann–Katoen 2018. The site separates the paper's encoded (allocation, action distribution) construction from the repo's default pure-action replacement wrapper.

Use the current implementation and maintained docs/AI notes when older prose conflicts:

shield_model_risk_budget reserves credible_delta inside the notebook's total max_risk; direct wrapper init_safety_bound is the model component. The older docs/concepts/probabilistic-shielding.md describes this less precisely. The website follows the current factory.
Default safety is robust over retained levels, but default replacement reward ranking is Bayesian. An older algorithm file in the paper still labels the replacement reward robust; the main paper definition and code have the current posterior-reward default.
patience <= 0 immediately commits to the estimate, possibly skipping a level; positive patience raises only one floor level per evidence window.
Credible floor is implemented as an ablation/diagnostic. Its posterior coverage assumption is not proved by smoothing a Bayesian update; the summable tail statement is conditional on calibration and true-level monotonicity. A reversal is logged, not repaired.
All-level robustness covers switching among the compiled induced kernels; arbitrary opponent actions require the separate exact adversarial audit.
The graph objective is time-free eventual unsafe reachability. Resets create new per-episode queries; this is not a lifetime-across-resets guarantee.

Verification and maintenance¶

The subsequent mathematical audit records checks against Edwin's paper and the AAMAS 2026 tutorial, the strict budget-boundary repair, the two added theory pages, and their guarantee qualifications. The updated-manuscript reconciliation documents randomised family-set certificates, fixed-floor permissiveness, count-centred outer sets and risk-dominance diagnostics at revision e049b7c. reconciliation-section.html and reconciliation.js add those four chapters; the builder embeds the latter as a fifth script. The warehouse solver still uses the pure robust Bellman operator. The current check suite passes 32,013 assertions; all thirteen chapters have been checked in Chromium and Firefox over isolated-file and HTTP loading.

node teaching-site/check.cjs checks analytic VI bounds, monotonicity, robust allocation feasibility across a grid of proposals, egalitarian filling, pairwise clipping/fallback, patience/reversal, tail sums and reward menus. Browser validation should cover each chapter over file:// and HTTP, desktop and phone widths, all controls, source navigation, reset/restart distinctions, and the credible-tail reversal diagnostic. Also check for console errors and horizontal overflow.

Run uv run python scripts/run_tests.py changed and the strict documentation build for repository changes. With documentation-only paths, the selector intentionally selects no pytest suites. There is no reason to run expensive trainer or graph integration tests for these isolated teaching assets.

The initial verification passed 7,326 mathematical assertions and Chromium interaction checks over both file:// and HTTP. All six chapters were checked at viewport widths 1440, 1024, 768, 390 and 320 pixels, with no page errors or horizontal page overflow. Screenshots were visually reviewed for desktop and phone layouts. The changed-test selector selected no pytest tests and the strict Zensical build passed. Keep the website README as .txt, and this note under a name distinct from the asset directory: the docs builder maps a same-named Markdown page and a directory README to the same index destination.

The source copy can be refreshed with the explicit file list in teaching-site/README.txt. Avoid deleting unrelated files in the user's local destination. A framework-based app or full kernel-backed simulator would add build and environment dependencies without improving these small examples; use the actual notebooks instead for trained-environment exploration.