Exact Distinguishability in Non-Markovian Decision Processes
This paper asks whether a fixed offline corpus generated by a behaviour policy can ever distinguish two candidate Regular Decision Processes (RDPs). It proves that when two candidates are $\pi$-observationally equivalent, their posterior odds remain frozen at the prior for any sample size (Theorem 6), gives an exact measure-zero characterization via the product-automaton blame language (Theorem 12), and derives PEC, a linear-time algorithm that certifies equivalence and names the missing experiment. The work matters because existing PAC offline guarantees for RDPs assume a distinguishability condition that was previously impossible to verify.
The paper makes a strong theoretical contribution by closing a verification gap in offline RDP learning. The frozen-posterior theorem and the linear-time decision procedure are rigorously formalized in Lean 4, and the application to RegORL's distinguishability assumption is concrete. However, the empirical evaluation is narrow: four small synthetic environments and a parameterized corridor family, with no standard partially observable RL benchmarks. The requirement of a known candidate pair also limits practical applicability. Nonetheless, for its stated scope, the paper is mathematically sound and algorithmically useful.
The core theoretical results are elegant and hold up well. Theorem 6 shows that $\pi$-observational equivalence freezes posterior odds at the prior. The T-maze example (Proposition 8) is a crisp counterexample showing that state coverage does not imply identifiability. Theorem 12 gives an exact measure-zero characterization via the blame language of the product automaton, and Corollary 13 yields a genuinely linear-time procedure independent of the horizon. The formal verification in Lean 4 adds confidence, and validation against brute-force enumeration on 3700 model pairs supports correctness.
The experimental evaluation is extremely limited in scope. All environments are synthetic, with at most a handful of automaton states, and no validation occurs on standard benchmarks such as POPGym, which the authors explicitly exclude from scope. The end-to-end evaluation reveals that for shallow separating horizons, designed experiments offer no advantage over uniform random exploration, undermining the practical urgency of the method except at large depths (Table 3). Several important limitations are deferred: continuous observations are out of scope, the exact test requires estimated tables to satisfy a tolerance window that shrinks as candidates near equivalence, and deciding identifiability within an implicitly specified hypothesis class remains open. The policy-deviation selection via expected information gain is exponential in the lookahead $\ell$, and PEC only supplies the required depth without reducing that cost.
The authors fairly position their work against Cipollone et al. (2023) and Deb et al. (2025), noting that prior work provides no method to verify its distinguishability assumption. Table 1 demonstrates that RegORL's $\mu_0$ is exactly zero on three of four environments, while PEC certifies equivalence and names the restoring experiment. The comparison is exact (rational arithmetic) rather than approximate. However, the paper does not compare against active automata learning methods that could query the system, acknowledging that the fixed-corpus setting differs. The brute-force validation on 3700 model pairs is convincing for the algorithmic component, though the real-world relevance of these pairs is unclear.
Reproducibility is generally strong. The authors release source code and Lean 4 formalizations. Experiments use exact rational arithmetic or well-specified Dirichlet priors, eliminating stochastic training variability. Hyperparameters (e.g., $\alpha=1$, horizons, action supports) are documented. The synthetic environments have known ground truth, making verification straightforward. The main barriers to independent reproduction are the lack of real-world data and the limited scale (environments bounded to at most five states for exact enumeration). An independent researcher could replicate the synthetic results exactly using the provided repository.
Non-Markovian environments are often modeled as Regular Decision Processes (RDPs), where dynamics depend on the interaction history through a finite automaton. Existing offline guarantees for RDPs rely on a distinguishability assumption on the behaviour policy but provide no means of verifying it. When the assumption is violated, distinct models may explain the data equally well. We study when data collected under a fixed behaviour policy can distinguish two candidate RDPs. We prove that the posterior odds between observationally equivalent candidates remain equal to the prior odds at every sample size, even when the policy visits every automaton state, and verify both results formally in Lean 4. We then characterize this equivalence exactly and derive PEC, an algorithm that decides it in time linear in the size of the product automaton. The distinguishability assumption of prior work fails on three of our four test environments, and the experiment identified by PEC restores it in each case.
Pick a starting point or write your own. Challenges run in the background, so you can keep reading while the AI investigates.
No challenges yet. Disagree with the review? Ask the AI to revisit a specific claim.