The Myhill-Nerode Theorem for Bounded Interaction: Canonical Abstractions via Agent-Bounded Indistinguishability

TL;DR

This paper generalizes the Myhill-Nerode theorem to bounded interaction scenarios in POMDPs, introducing a canonical quotient that captures indistinguishability under capacity limits, with practical experiments validating its properties.

Contribution

It formalizes a Myhill-Nerode type theorem for bounded agents in POMDPs, defining a canonical, minimal quotient that characterizes agent indistinguishability and decision sufficiency.

Findings

The quotient is canonical, minimal, and unique.

Clock-aware probes achieve decision-sufficiency for certain objectives.

Empirical validation on Tiger and GridWorld supports theoretical claims.

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.