Exact Distinguishability in Non-Markovian Decision Processes
Kabir Murjani, Nisarg Patel
cs.LG
Oct 1, 2026 · v1
cs.AI stat.ML
TL;DR
Key theorems on frozen posterior odds and the T-maze counterexample to state coverage are machine-checked in a released Lean 4 development.
Abstract
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.
Problem
Offline learning guarantees for Regular Decision Processes rely on a distinguishability assumption on the behaviour policy, but there is no way to check it. When it fails, distinct candidate models can explain the data equally well.
Approach
The authors define policy-relative observational equivalence between two candidate RDPs. They prove that posterior odds between equivalent candidates stay at the prior odds, and they give a two-action T-maze showing that state coverage does not imply distinguishability. Both results are verified in Lean 4. They characterize equivalence through disagreeing state-action pairs of the product automaton and a regular blame language, which yields PEC, a decision procedure linear in the product size that also names a separating experiment.
Results
The distinguishability assumption of prior work fails on three of four test environments. The experiment identified by PEC restores separating mass in each case.
| Environment | T | mass under π | mass under π′ | Assumption 2 | PEC |
|---|
| T-maze | 2 | 0 | 1/2 | fails | equivalent |
| Rotating MAB | 3 | 0 | 245/512 | fails | equivalent |
| Cheat MAB | 3 | 0 | 1/9 | fails | equivalent |
| Rotating Maze | 4 | 0 | 1/8 | holds (trivially) | equivalent |
Separating mass under behaviour policy π and PEC-designed policy π′