The Myhill-Nerode Theorem for Bounded Interaction: Canonical Abstractions via Agent-Bounded Indistinguishability
Organizations: DefSig
Abstract
Any capacity-limited observer induces a canonical quotient on its environment: two situations that no bounded agent can distinguish are, for that agent, the same. We formalise this for finite POMDPs. A fixed probe family of finite-state controllers induces a closed-loop Wasserstein pseudometric on observation histories and a probe-exact quotient merging histories that no controller in the family can distinguish. The quotient is canonical, minimal, and unique-a bounded-interaction analogue of the Myhill-Nerode theorem. For clock-aware probes, it is exactly decision-sufficient for objectives that depend only on the agent's observations and actions; for latent-state rewards, we use an observation-Lipschitz approximation bound. The main theorem object is the clock-aware quotient; scalable deterministic-stationary experiments study a tractable coarsening with gap measured on small exact cases and explored empirically at larger scale. We validate theorem-level claims on Tiger and GridWorld. We also report operational case studies on Tiger, GridWorld, and RockSample as exploratory diagnostics of approximation behavior and runtime, not as theorem-facing evidence when no exact cross-family certificate is available; heavier stress tests are archived in the appendix and artifact package.
Figures & tables
| Tier | Representative results | What the tier supports | Certificate type |
|---|---|---|---|
| Tier I: theorem-aligned exact | Tables 2 , 3 , 4 | Theorem-level statements about on the stated bounded exact cases, including measured cross-family transfer on tractable exact instances | Exhaustive clock-aware enumeration on the stated finite benchmark and horizon |
| Tier II: operational exact-for-family | Table 5 | Exact statements about the operational family and controller-subset certification within that family | Full deterministic-stationary FSC tensor together with reported certificate |
| Tier III: operational empirical scaling | Tables 6 , 13 , 10 , 11 | Compression, stability, and runtime evidence for the tractable operational quotient ; not theorem validation for unless an explicit bridge is reported | Sampling confidence intervals, ARI checks, runtime reporting, and explicit disclosure when no theorem-level certificate is available |
| Benchmark | ARI | Obs. value changed? | ||||
|---|---|---|---|---|---|---|
| Tiger | 2 | 4 | 4 | 1.000 | 0.490 | No |
| Tiger | 4 | 11 | 16 | 0.961 | 1.315 | No |
| Tiger | 6 | 22 | 64 | 0.953 | 2.077 | No |
| Tiger | 8 | 37 | 256 | 0.956 | 2.795 | No |
| Tiger | 10 | 56 | 1024 | 0.959 | 3.499 | No |
| GridWorld 3x3 | 2 | 6 | 6 | 1.000 | 0.347 | No |
| Benchmark | Obj. | Hist. | Cls. | Policy | Regret | |||||
|---|---|---|---|---|---|---|---|---|---|---|
| Tiger | Obs score | 2 | 7 | 4 | 0.000 | 0.000 | L L | 1.000 | 1.000 | 0.000 |
| Tiger | Action+obs score | 2 | 7 | 4 | 0.000 | 0.000 | OL OL | 1.000 | 1.000 | 0.000 |
| Tiger | Obs score | 4 | 31 | 16 | 0.001 | 0.003 | L L L L | 2.000 | 2.000 | 0.000 |
| Tiger | Action+obs score | 4 | 31 | 16 | 0.001 | 0.003 | OL OL OL OL | 2.000 | 2.000 | 0.000 |
| Tiger | Obs score | 6 | 127 | 64 | 0.008 | 0.132 | L L L L L L | 3.000 | 3.000 | 0.000 |
| Tiger | Action+obs score | 6 | 127 | 64 | 0.009 | 0.139 | OL OL OL OL OL OL | 3.000 | 3.000 | 0.000 |
| Benchmark | Reward | Hist. | Cls. | Policy | Regret | |||||
|---|---|---|---|---|---|---|---|---|---|---|
| Tiger | Tiger reward | 2 | 7 | 4 | 0.000 | 0.000 | L L | -2.000 | -2.000 | 0.000 |
| Tiger | Tiger reward | 4 | 31 | 16 | 0.000 | 0.009 | L L L L | -4.000 | -4.000 | 0.000 |
| Tiger | Tiger reward | 6 | 127 | 64 | 0.005 | 0.386 | L L L L L L | -6.000 | -6.000 | 0.000 |
| Tiger | Tiger reward | 8 | 511 | 256 | 0.061 | 19.515 | L L L L L L L L | -8.000 | -8.000 | 0.000 |
| Tiger | Tiger reward | 10 | 2047 | 1024 | 0.663 | 1549.370 | L L L L L L L L L L | -10.000 | -10.000 | 0.000 |
| GridWorld 3x3 | Goal reward | 2 | 21 | 6 | 0.000 | 0.001 | D U | 0.311 | 0.311 | 0.000 |
| Benchmark | Op. exact classes | Approx. classes | ARI | |||
|---|---|---|---|---|---|---|
| Tiger ( ) | 0.0 | 1 | 0.980 | 16 | 11 | 0.961 |
| Tiger ( ) | 0.0 | 3 | 0.245 | 16 | 15 | 0.994 |
| Tiger ( ) | 0.0 | 5 | 0.000 | 16 | 16 | 1.000 |
| GridWorld ( ) | 0.3 | 1 | 0.233 | 6 | 4 | 0.981 |
| GridWorld ( ) | 0.3 | 3 | 0.000 | 6 | 6 | 1.000 |
| GridWorld ( ) | 0.3 | 5 | 0.000 | 6 | 6 | 1.000 |
| Benchmark | Cache (s) | 95% CI on | |||||
|---|---|---|---|---|---|---|---|
| GridWorld | 64 | 6 | 6 | 4 | 3 | 0.28 | |
| GridWorld | 100 | 6 | 6 | 4 | 3 | 0.30 | |
| RockSample | 257 | 5 | 5 | 4 | 3 | 0.48 | |
| Random | 50 | 6 | 3 | 3 | 3 | 0.22 | |
| Random | 100 | 6 | 3 | 3 | 3 | 0.35 |
| Benchmark | Quotient | PBVI orig (s) | PBVI quot (s) | Speedup | Value gap | |
|---|---|---|---|---|---|---|
| Tiger | 2 | 3 | 0.001 | 0.001 | 0.00 | |
| GridWorld | 9 | 6 | 0.003 | 0.002 | 0.00 | |
| GridWorld | 25 | 5 | 0.008 | 0.003 | 0.00 | |
| Net. Monitor ( ) | 16 | 4 | 0.005 | 0.002 | 0.00 | |
| RockSample | 257 | 3 | 0.092 | 0.004 | 0.00 |
Appendix figures & tables27 assets
Supplementary material from the paper’s appendix.
Appendix
| Dimension | State bisimulation | PSRs / OOMs | This work |
|---|---|---|---|
| Abstraction target | States | Predictive statistics | Observation histories |
| Distinguishing power | All policies / actions | Open-loop test sequences | Bounded controller family |
| Comparison object | One-step transitions | Linear predictors | Finite-horizon observation laws |
| Loop type | Open-loop (per-action) | Open-loop | Closed-loop |
| Quotient output | State partition | Low-rank representation | History partition quotient POMDP |
| Tier | Verification target | Command / artifact path | Serial budget and role |
|---|---|---|---|
| I | Theorem tables plus operational core through Table 6 | pythonpaper/generate_theory_first_tables.py and python-mexperiments.run_basic_results--profilequick--seed7--no-parallel | min; intended reviewer verification target. |
| II | Long-horizon extension (Tables 10 , 11 , Figures 4 , 5 ) | Add --include-hierarchical-scaling--max-horizon10 to the operational driver | min serial; horizon-scaling narrative only. |
| III | Heaviest stress rows (Tables 13 , 14 ) | Same driver for rerunning; artifact-only: pythonartifacts/tier3/verify_tier3_artifacts.py | – s per row, up to 2 h for largest ; archival. Verifier: s. |
| Method | Segment | Layers | Runtime (s) | Histories processed | |
|---|---|---|---|---|---|
| 4 | Direct | – | 1 | 0.05 | 31 |
| 4 | Layered | 4 | 1 | 0.05 | 31 |
| 6 | Direct | – | 1 | 0.96 | 127 |
| 6 | Layered | 4 | 2 | 0.05 | 38 |
| 8 | Direct | – | 1 | 16.42 | 511 |
| 8 | Layered | 4 | 2 | 0.10 | 62 |
| Method | FSCs used | Runtime (s) | Classes | ARI vs. full | |
| 4 | Full op.-exact | 147 | 2.53 | 10 | 1.000 |
| 5 | Full op.-exact | 147 | 10.95 | 16 | 1.000 |
| 6 | Full op.-exact | 147 | 46.11 | 30 | 1.000 |
| 7 | Full op.-exact | 147 | 194.27 | 50 | 1.000 |
| 7 | Calibrated subset (empirical) | 10 | 12.96 | 50 | 0.9997 |
| 8 | Calibrated subset (empirical) | 10 | 53.69 | 77 | – |
| Dimension | Growth | Technique | Demonstrated |
|---|---|---|---|
| States | per belief | Sampling-based | (sampling), (sampling) |
| FSCs | Greedy FSC subsets | Certified: , scaling: FSCs on RockSample Empirical: calibrated subset | |
| Histories | Exp. in | Layered horizon decomposition | Direct to ; layered to |
| Observations | histories | -coarsening (Prop. 5.5 ) | GridWorld obs |
| Track | Benchmark | Method | Runtime (s) | 95% CI on | |||||
|---|---|---|---|---|---|---|---|---|---|
| Scale-up | Net. Mon. ( ) | 4,096 | 3 | 2 | Sampling | 13 | 5 | ||
| Large | Random | 2,000 | 10 | 2 | Sampling | 111 | 10 | ||
| Long | Net. Mon. ( ) | 1,024 | 3 | 20 | Layered | 13 | 5 |
| Benchmark | FSCs | Runtime (s) | 95% CI on | |||||||
|---|---|---|---|---|---|---|---|---|---|---|
| RockSample | 257 | 1 | 2 | 9 | 5 | 5 | 4 | 3 | 0.5 | |
| RockSample | 257 | 2 | 2 | 5,193 | 5 | 5 | 5 | 5 | 321 | |
| Net. Mon. ( ) | 16 | 1 | 3 | 5 | 14 | 9 | 6 | 5 | 1.1 | |
| Net. Mon. ( ) | 16 | 2 | 3 | 1,605 | 14 | 14 | 14 | 6 | 353 | |
| Net. Mon. ( ) | 512 | 1 | 2 | 10 | 5 | 5 | 4 | 3 | 11 | |
| Net. Mon. ( ) | 512 | 2 | 2 | 6,410 | 5 | 5 | 5 | 3 | 6,802 |
| Classes | Compression | Policies | ||
|---|---|---|---|---|
| 1 | 0.0 | 6 | 0.29 | 5 |
| 1 | 0.2 | 5 | 0.24 | 5 |
| 1 | 0.35 | 3 | 0.14 | 5 |
| 1 | 0.5 | 3 | 0.14 | 5 |
| 2 | 0.0 | 6 | 0.29 | 6,405 |
| 2 | 0.2 | 6 | 0.29 | 6,405 |
| Empirical error | Prop A.1 | ||||
| Panel A: Tiger, synthetic | |||||
| 0.0 | 0.00 | 0.00 | 0.00 | 0.0 | |
| 0.1 | 0.00 | 0.20 | 0.00 | 3.4 | |
| 0.3 | 0.00 | 0.60 | 0.00 | 10.2 | |
| 0.5 | 0.12 | 0.24 | 1.00 | 0.49 | 17.0 |
| Panel B: Tiger, standard reward (vacuous) | |||||
| Min cl. | Max cl. | Min val. err. | Max val. err. | |
|---|---|---|---|---|
| 0.0 | 7 | 7 | 0.000 | 0.000 |
| 0.2 | 5 | 7 | 0.000 | 0.000 |
| 0.4 | 3 | 7 | 0.000 | 0.108 |
| 0.6 | 3 | 3 | 0.058 | 0.145 |
| Benchmark | Method | Classes | Val. err. | Time (s) | ||
| Tiger full actions | ||||||
| -quotient | 0.3 | 4 | 0.000 | 0.000 | ||
| Truncation ( ) | 0.3 | 5 | 0.000 | 0.000 | ||
| Random partition | 0.3 | 3.7 | 0.041 | 0.082 | ||
| Belief-distance | 0.3 | 6 | 0.000 | 0.000 | ||
| Bisimulation | 0.3 | 6 | 0.000 | 0.000 | 0.05 | |
| Ablation | Variant | Classes ( ) | Note |
|---|---|---|---|
| Metric | (discrete ) | 7 | Default |
| TV-equivalent | 7 | Same on Tiger (binary ) | |
| Memory | (3 FSCs) | 7 | Coarser |
| (147 FSCs) | 14 | Finer, 0 value error | |
| Approx. | Full enum. (147 FSCs) | 14 | Exact |
| Greedy | 14 | ARI , faster |
| Benchmark | Depth | FSCs | Rank (90%) | Rank (95%) | Rank (99%) | |
|---|---|---|---|---|---|---|
| Tiger ( ) | 1 | 3 | 3 | 1 | 1 | 1 |
| Tiger ( ) | 2 | 3 | 147 | 3 | 4 | 7 |
| Grid ( ) | 1 | 1 | 5 | 1 | 2 | 4 |
| Grid ( ) | 2 | 1 | 6,405 | 2 | 3 | 5 |
| Benchmark | |||||||
|---|---|---|---|---|---|---|---|
| Grid | 2 | 6 | 6 | 5 | 4 | 3 | 3 |
| Grid | 3 | 22 | 16 | 12 | 9 | 6 | 5 |
| Random | 2 | 6 | 3 | 3 | 3 | 3 | 3 |
| Random | 3 | 22 | 4 | 4 | 4 | 4 | 4 |
| Grid | Classes | Compression | Time (s) | |
|---|---|---|---|---|
| 9 | 4 | 0.03 | ||
| 16 | 4 | 0.04 | ||
| 25 | 4 | 0.05 | ||
| 36 | 4 | 0.07 |
| Experiment | Time (s) |
|---|---|
| Tiger reproduction | |
| Capacity sweep | – |
| Value loss bounds | – |
| Metric sensitivity | – |
| Baseline comparison | – |
| Low-rank analysis | – |
| Benchmark | FSCs | Enum (s) | Cache (s) | Cache % | ||
|---|---|---|---|---|---|---|
| Tiger | 2 | 1 | 3 | |||
| GridWorld | 9 | 1 | 5 | |||
| RockSample(4,4) | 257 | 1 | 9 |
| Trajectories | Mean ARI | Min ARI | Replications |
|---|---|---|---|
| 50 | 0.991 | 0.961 | 5 |
| 100 | 0.994 | 0.971 | 5 |
| 250 | 0.994 | 0.971 | 5 |
| 500 | 0.998 | 0.971 | 5 |
| 1,000 | 0.994 | 0.971 | 5 |
| Mean classes | Std | Min | Max | |
|---|---|---|---|---|
| 0.0 | 6.0 | 0.0 | 6 | 6 |
| 0.1 | 6.0 | 0.0 | 6 | 6 |
| 0.25 | 4.0 | 0.0 | 4 | 4 |
| 0.45 | 3.0 | 0.0 | 3 | 3 |
| Trajectories | Coverage | Mean CI width |
|---|---|---|
| 100 | ||
| 250 | ||
| 500 |
| Benchmark | ||||||
|---|---|---|---|---|---|---|
| Hallway ( ) | 10 | 3 | 3 | 5 | 5 | 3 |
| Hallway ( ) | 20 | 3 | 3 | 5 | 5 | 3 |
| Network ( ) | 16 | 5 | 3 | 5 | 4 | 3 |
| Network ( ) | 32 | 6 | 3 | 5 | 4 | 3 |
| Benchmark | Policies | Classes | Value gap | |||
| Tiger | 1 | 0.0 | 3 | 4 | 0.373 | 0.000 |
| Tiger | 1 | 0.3 | 3 | 4 | 0.373 | 0.000 |
| Tiger | 1 | 0.5 | 3 | 3 | 0.373 | 0.000 |
| Tiger | 2 | 0.3 | 147 | 4 | 0.373 | 0.000 |
| Tiger | 2 | 0.5 | 147 | 3 | 0.373 | 0.000 |
| Hallway | 1 | 0.0 | 3 | 5 | 0.262 | 0.000 |
| (classes / ARI) | (classes / ARI) | (classes / ARI) | |
|---|---|---|---|
| 0.5 | 4 / 1.00 | 4 / 1.00 | 3 / 1.00 |
| 0.3 | 4 / 1.00 | 4 / 1.00 | 3 / 1.00 |
| 0.1 | 4 / 1.00 | 3 / 0.89 | 3 / 1.00 |
| 0.7 | 4 / 1.00 | 4 / 1.00 | 3 / 1.00 |
| 0.9 | 4 / 1.00 | 3 / 0.89 | 3 / 1.00 |
| Symbol | Meaning |
|---|---|
| Finite POMDP | |
| State, action, observation sets | |
| Transition kernel | |
| Observation kernel | |
| Reward function | |
| Belief state at time |
Partially Observable Markov Decision Processes
Partially Observable Markov Decision Processes study sequential decisions when agents must act from incomplete, noisy observations of hidden states.
See all 88 papers