Paper deep dive
Exact Distinguishability in Non-Markovian Decision Processes
Kabir Murjani, Nisarg Patel
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 94%
Last extracted: 10/3/2026, 3:25:27 AM
Summary
This paper addresses the problem of distinguishing between two candidate Regular Decision Processes (RDPs) in non-Markovian environments using data collected under a fixed behavior policy. The authors prove that if two RDPs are 'pi-observationally equivalent' (assigning equal likelihood to all histories generated by the policy), the posterior odds between them remain equal to the prior odds regardless of sample size. They introduce PEC, an algorithm that decides this equivalence in time linear with respect to the product automaton size by checking reachability of disagreeing state-action pairs. Experiments show that prior distinguishability assumptions often fail, and PEC can identify specific experiments to restore distinguishability.
Entities (7)
Relation Signals (5)
PEC → decides → pi-observational equivalence
confidence 98% · derive PEC, an algorithm that decides it in time linear in the size of the product automaton.
PEC → hastimecomplexity → linear in the size of the product automaton
confidence 95% · decides it in time linear in the size of the product automaton.
Regular Decision Process → models → Non-Markovian environments
confidence 95% · Non-Markovian environments are often modeled as Regular Decision Processes (RDPs)
RegORL → proposedby → Cipollone et al.
confidence 92% · Cipollone et al. (2023) gave the first provably efficient offline algorithm for RDPs, RegORL
Lean 4 → usedtoverify → theoretical results
confidence 90% · verify both results formally in Lean 4.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
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.
Tags
Links
- Source: https://arxiv.org/abs/2610.01527v1
- Canonical: https://arxiv.org/abs/2610.01527v1
Trouble viewing inline? Open PDF directly →
Full Text
114,730 characters extracted from source content.
Expand or collapse full text
Exact Distinguishability in Non-Markovian Decision Processes Kabir Murjani Nisarg Patel Nirma University Ahmedabad, India kabirmurjani@gmail.com Google Mountain View, CA nisargpatel@google.com 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.11 1 Source code and Lean 4 formalisations. 1 Introduction To model non-Markovian environments, recent work frequently utilizes the Regular Decision Process (RDP) (Brafman and De Giacomo, 2019), a framework where the next observation depends on the entire interaction history through the state of a finite automaton driven by the action-observation sequence. The model class sits between Markov decision processes (MDPs) and partially observable Markov decision processes (POMDPs), and a recent line of work learns it offline, from a corpus of interaction data produced under a fixed operating policy. A corpus of that kind is consistent with several environments at once. A point estimator fitted to it returns one of them with no indication that the others fit equally well, and a Bayesian learner’s odds between them remain at the prior, which from inside a single run cannot be told apart from slow learning. Existing guarantees for this model class presuppose that the corpus is informative. Cipollone et al. (2023) gave the first provably efficient offline algorithm for RDPs, RegORL, with probably approximately correct (PAC) guarantees under a distinguishability assumption on the behaviour policy, and Deb et al. (2025) replace that parameter, which decays exponentially in the number of automaton states, with a formal-language metric. Neither gives a way to check whether a given policy satisfies the assumption. Consider a freight planner who reroutes around a lane for one period after each late delivery on it. The records contain the lane and contain late deliveries, yet a model in which lateness persists into the next period and one in which it does not agree on every shipment the rule sends. No quantity of such records therefore tests the belief that motivated the rule, although a single shipment sent on the lane just after a late delivery would test it. Given two candidate models and a behaviour policy, we investigate whether any quantity of data collected under that policy can distinguish between them, and if not, we identify which experiment would separate them. The question is posed for a stated pair. Such pairs arise as competing mechanistic accounts already written down in a domain, as a hypothesis tested against its memoryless null, or as the top modes of a Bayesian structure learner compared pairwise. Deciding identifiability over an implicitly specified hypothesis class is a different problem and remains open (§7). Whether data collected under the behaviour policy can separate two candidates is determined by the candidates and the policy alone. We decide it exactly, before any learner is fitted, and the answer applies to a corpus of any size. The relevant notion is π-observational equivalence: two candidates that assign equal likelihood to every history the behaviour policy can generate leave the posterior odds between them at the prior odds at every sample size (Theorem 6). The condition differs from state coverage. On a two-action T-maze the behaviour policy visits every state while the posterior never moves (Proposition 8), and both results are checked in Lean 4 against Mathlib (§4). Characterizing π-equivalence exactly depends on choosing the right object (§5). The set of histories on which two likelihoods differ need not be regular, since two products of real numbers may coincide arithmetically, so it admits no decision procedure of the usual kind. Posing the question instead over the disagreeing state–action pairs of the product automaton yields a characterization that holds for an arbitrary behaviour policy, at every finite horizon and at infinite horizon (Theorem 12). When the action support of the policy does not vary with history, that characterization reduces to reachability in the product automaton, and the resulting procedure, Pec (the π-equivalence certifier), decides it in time O(|Q||Q′‖A‖O|)O(|Q|\,|Q |\,|A|\,|O|), independently of the horizon (§5.3). When the candidates are not equivalent, Pec returns the state pair and the action at which the corpus must be extended, which is the missing experiment itself. It agrees with brute-force enumeration of histories on all 3700 model pairs we tested, and its running time grows linearly in the size of the product automaton up to 10610^6 state pairs. The same search answers the question that prior offline guarantees leave open. The distinguishability assumption on which the guarantee of Cipollone et al. (2023) rests takes time exponential in the horizon to evaluate from its definition, whereas Pec decides it without reference to the horizon (§6.1). Computed in exact arithmetic, the distinguishability parameter is zero on three of our four test environments, each of which Pec certifies as equivalent, and in every case the experiment named by the witness restores the assumption. 2 Related Work Non-Markovian formalisms. Reward machines place history dependence in the reward alone and leave the dynamics Markov (Toro Icarte et al., 2022; Varricchione et al., 2025). Regular Decision Processes (Brafman and De Giacomo, 2019) make the dynamics themselves history dependent, and Abadi and Brafman (2020) gave the first method for learning and solving them. Subsequent work covers offline reinforcement learning with PAC guarantees (Cipollone et al., 2023; Deb et al., 2025; Deb et al., 2024), Markov abstractions (Ronca et al., 2022), online learning of non-Markovian reward models (Rens et al., 2020), task automata (Abate et al., 2023), and automata cascades (Ronca et al., 2023). Offline guarantees. Cipollone et al. (2023) established the first provably efficient offline reinforcement learning framework for this model class, with a sample complexity parameterized by a distinguishability quantity μ0 _0 that the corpus is assumed to bound away from zero. That assumption is the natural counterpart of our question, and we compute their parameter exactly (§6.1). The two methods return different objects, since RegORL returns a policy with a bound conditional on identifiability while Pec returns identifiability itself. Appendix S5.2 discusses that comparison in full. Automata learning and non-identifiability. LMDP∗L^*_MDP (Tappler et al., 2021) learns MDP structure from black-box interaction and already designs schedulers to disambiguate, and practical frameworks answer equivalence queries by statistical conformance testing (Muskardin et al., 2022). The barrier in our setting is the absence of a system to query, since conformance testing still has to run new traces while we hold a fixed corpus, and the setting of those methods is Markov given the state (Fica and Otop, 2025; Fortz et al., 2026). Priors over automata exist (Pfau et al., 2010; Shibata and Yoshinaka, 2014; Umili and Capobianco, 2024) but model sequences without actions or a behaviour policy, and Bayesian treatments of non-Markovian reward keep the history dependence in the reward (Topper et al., 2024; Dohmen et al., 2021; Zhu et al., 2026). Freezing under an uninformative likelihood is known in off-policy evaluation and causal inference (Parbhoo et al., 2022; Takahashi, 2026; Fu et al., 2022). In a Markov MDP, non-identifiability under a behaviour policy is a state–action coverage condition on the true model. Expected information gain (Houlsby et al., 2011) has not been combined with priors over automaton structure, and the theory of contaminated priors and misspecified posteriors that we rely on is classical (Berk, 1966; Shalizi, 2009). 3 Preliminaries This framework requires no independent reward function, since a reward taking finitely many values is naturally subsumed into O by O=Oenv×RO=O_env× R, with e(q,a)e(q,a) acting as the joint emission over the pair. 3.1 Regular decision processes Fix finite sets A of actions and O of observations. A history is a finite sequence h=(a1,o1)⋯(aT,oT)∈(A×O)∗h=(a_1,o_1)·s(a_T,o_T)∈(A× O)^*, and we write ℋ=(A×O)∗H=(A× O)^* and ℋTH_T for histories of length T. For 1≤t≤|h|+11≤ t≤|h|+1 we write h<t=(a1,o1)⋯(at−1,ot−1)h_<t=(a_1,o_1)·s(a_t-1,o_t-1) for the prefix of length t−1t-1, with h<1=λh_<1=λ the empty history. Definition 1 (RDP). An RDP is a tuple M=(Q,q0,δ,e)M=(Q,q_0,δ,e) where Q is a finite set of automaton states, q0∈Qq_0∈ Q is initial, δ:Q×A×O→Qδ:Q× A× O→ Q is the transition function, and e:Q×A→Δ(O)e:Q× A→ (O) assigns to each state–action pair a distribution over observations, so that ∑o∈Oe(q,a)(o)=1 _o∈ Oe(q,a)(o)=1 for every (q,a)(q,a). The automaton state is a deterministic function of history. We extend δ to δ^:ℋ→Q δ:H→ Q by δ^(λ)=q0 δ(λ)=q_0 and δ^(h(a,o))=δ(δ^(h),a,o) δ(h\,(a,o))=δ( δ(h),a,o). The set Q is not observable, and the agent sees only the history h. Definition 1 carries no separate reward function, since a reward taking finitely many values is subsumed in O by setting O=Oenv×RO=O_env× R and reading e(q,a)e(q,a) as the joint emission over the observed pair. Appendix S6.5 gives that correspondence in full. Definition 2 (History likelihood). LM(h)=∏t=1|h|e(δ^(h<t),at)(ot) L_M(h)\;=\; _t=1^|h|e ( δ(h_<t),a_t )(o_t), the probability that M emits the observations in h given the actions in h. The likelihood LML_M conditions on the actions and excludes the policy’s own probabilities. This factorization carries the develorequires a logarithm, so expected information gain alonepment that follows, and it rests on an ordering assumption that §5 depends upon, namely that the policy chooses ata_t before observing oto_t. Definition 3 (Policy and induced path measure). A behaviour policy is π:ℋ→Δ(A)π:H→ (A). Its history probability is Π(h)=∏t=1|h|π(h<t)(at) (h)= _t=1^|h|π(h_<t)(a_t), and the induced measure on histories is ℙMπ(h)=Π(h)LM(h)P^π_M(h)= (h)\,L_M(h). 3.2 Two notions of observational equivalence Definition 4 (Global observational equivalence). M∼M′M M iff LM(h)=LM′(h)L_M(h)=L_M (h) for every h∈ℋh . Definition 5 (π-observational equivalence). M∼πM′M _πM iff LM(h)=LM′(h)L_M(h)=L_M (h) for every h with Π(h)>0 (h)>0, that is, for every history the behaviour policy can generate. Both relations are equivalence relations, M∼M′M M implies M∼πM′M _πM for every π, and either relation implies ℙMπ=ℙM′πP^π_M=P^π_M . We formalise these facts in Lean together with the reflexivity, symmetry, and transitivity lemmas that each relation requires. Throughout, the unqualified term observational equivalence denotes the policy-relative notion of Definition 5, and the relation of Definition 4 is always marked global. Global equivalence is strictly stronger, and §4.1 exhibits a pair that is π-equivalent while globally inequivalent. 4 Policy-Relative Identifiability Let a prior assign weights w,w′>0w,w >0 to M,M′M,M respectively. After observing history h, the unnormalized posterior weights are wLM(h)w\,L_M(h) and w′LM′(h)w \,L_M (h). Theorem 6 (Frozen posterior odds). Let M∼πM′M _πM and let h be any history with Π(h)>0 (h)>0 and LM′(h)≠0L_M (h)≠ 0. Then wLM(h)w′LM′(h)=w′. w\,L_M(h)w \,L_M (h)\;=\; ww . Consequently the posterior odds between M and M′M equal the prior odds at every sample size, and no quantity of data collected under π moves them. Proof. π-equivalence gives LM(h)=LM′(h)L_M(h)=L_M (h), and the common nonzero factor cancels. ∎ Should the favoured candidate be π-equivalent to the truth, no data gathered under that behaviour policy can correct the fitted model. Correcting it becomes a problem of experimental design, which §6.2 takes up. The quantity our tables report is the complement of π-equivalence, namely the probability that the policy places on histories separating the pair. Definition 7 (Separating mass). Write DT=h∈ℋT:LM(h)≠LM′(h)D_T=\\,h _T:L_M(h)≠ L_M (h)\,\ for the histories of length T that the two models score differently. The separating mass of π at horizon T is the prior-predictive probability of that set, the prior weights being normalized so that w+w′=1w+w =1: mT(π)=∑h∈DTΠ(h)(wLM(h)+w′LM′(h)).m_T(π)\;=\; _h∈ D_T (h)\, (w\,L_M(h)+w \,L_M (h) ). Every entry labelled a mass is mT(π)m_T(π), computed in exact rational arithmetic at w=w′=1/2w=w =1/2. It vanishes at every horizon exactly when M∼πM′M _πM , since no history in DTD_T has both likelihoods zero, and hence exactly when the criterion of Theorem 12. 4.1 A two-action T-maze A natural guess is that π-observational equivalence reduces to state coverage, so that a policy visiting every automaton state of the true model identifies it. The following construction refutes that guess. It needs two actions, and no one-action variant can exhibit the phenomenon (Remark 16). • waitwait is uninformative, and both models emit a fair coin. • runrun runs the corridor through to its far end, whereupon the cue model reveals the remembered cue deterministically while the blind model emits a fair coin. The cue model McueM_cue has three automaton states and remembers the first observation, whereas the blind model MblindM_blind has a single state qbq_b and ignores history. The behaviour policy waits at every step. Proposition 8 (Collapse test). Under the always-waitwait policy, Mcue∼πMblindM_cue _πM_blind, yet Mcue≁MblindM_cue M_blind, and the policy reaches each of the two cue-tracking automaton states with probability 1/21/2. The separating history is (wait,left)(run,right)(wait,left)\,(run,right), on which the cue model assigns likelihood 00 and the blind model 1/41/4. We formalise this construction in Lean, proving π-equivalence under the wait policy, global inequivalence, the fact that the policy reaches both automaton states, and Theorem 6 applied to this pair. The construction exhibits full state coverage together with complete failure of identification. 5 Deciding π-Equivalence This section identifies the criterion that Proposition 8 separates from state coverage. The natural first conjecture, stated over the set of histories on which the likelihoods differ, is true, but that set need not be regular, so the conjecture yields no decision procedure (Appendix S6.6). 5.1 Product automaton Fix M=(Q,q0,δ,e)M=(Q,q_0,δ,e) and M′=(Q′,q0′,δ′,e′)M =(Q ,q_0 ,δ ,e ) and form the product automaton M×M′M× M on state set Q×Q′Q× Q , with initial state (q0,q0′)(q_0,q_0 ) and transition ((q,q′),a,o)↦(δ(q,a,o),δ′(q′,a,o)) ((q,q ),a,o ) (δ(q,a,o),\,δ (q ,a,o) ). Each history h drives it to a unique pair Δ^(h)∈Q×Q′ (h)∈ Q× Q . Definition 9 (Action support). The action support of the behaviour policy is Aπ=a∈A:π(h)(a)>0 for some h with Π(h)>0A_π=\\,a∈ A:π(h)(a)>0 for some h with (h)>0\,\, the set of actions π can ever take. Assumption 10 (History-independent action support). The action support does not vary with history, so π(h)(a)>0π(h)(a)>0 for every a∈Aπa∈ A_π and every h with Π(h)>0 (h)>0. Assumption 10 is not required by Theorem 12, which weights every candidate blame step by the probability the policy assigns to it. It is required by Corollary 13 and by Algorithm S1, which test a state pair without such a weight. Every policy in our suite satisfies it, and Remark 18 gives the reduction for a policy whose support does vary. Definition 11 (Disagreeing pairs and the blame language). The set of disagreeing pairs, indexed by the action that witnesses the disagreement, is Bπ=((q,q′),a) B_π\;=\; \\,((q,q ),a) ∈(Q×Q′)×Aπ:∃o∈O ∈(Q× Q )× A_π\;:\;∃\,o∈ O with e(q,a)(o)≠e′(q′,a)(o), e(q,a)(o)≠ e (q ,a)(o)\, \, and the blame language is LBπ=h(a,o)∈ℋ:(Δ^(h),a)∈Bπ,L_B_π\;=\; \\,h\,(a,o) \;:\; ( (h),\,a )∈ B_π\, \, the histories drive the product automaton into a disagreeing pair and take the action on which it disagrees. Restricting the quantifier to AπA_π makes the pair test policy-relative, and carrying the trailing action weights each candidate blame step by π(h)(a)π(h)(a). Appendix S6.5 shows why each device is needed. The set BπB_π depends only on the two emission tables and the action support, so deciding membership is a finite check that involves no products of probabilities, and LBπL_B_π is recognized by M×M′M× M with an accepting condition on state pair and action. The blame language is therefore regular by construction, and it is the object over which the question should be posed. Relation to classical equivalence checking. The product is the construction that decides deterministic finite automaton (DFA) equivalence (Hopcroft and Karp, 1971) and probabilistic bisimulation (Larsen and Skou, 1991; Givan et al., 2003), but the question asked of it differs in the two devices above. Those notions quantify over every input, so each refines global equivalence (Definition 4) and each calls the pair of Proposition 8 distinguishable. That verdict is correct about the two automata, but the corpus exhibits no such distinction at any sample size. The trailing action and the action-before-observation ordering also keep the blame-step weight Π(h)π(h)(a) (h)\,π(h)(a) common to both models, so no policy can obtain a certificate by weighting the disagreeing step unevenly under the two candidates (Appendix S6.5). Bisimulation metrics (Ferns et al., 2004) measure how far apart two states of one model are and do not condition on a policy. The quantitative refinement here is instead the separation γ of §5.4. 5.2 The characterization at finite horizon Both models assign LBπL_B_π the same probability under π (Appendix S6.5), so we write ℙπ(LBπ)P^π(L_B_π) without a model subscript. Theorem 12 (Measure-zero characterization). M∼πM′M _πM if and only if ℙπ(LBπ)=0P^π(L_B_π)=0, that is, if and only if the behaviour policy assigns probability zero to ever driving the product automaton into a disagreeing pair and there taking an action on which the two emission rows differ. The statement holds at every finite horizon T, for histories of length at most T, and at infinite horizon, for the event that some prefix of the trajectory lies in LBπL_B_π. The behaviour policy is arbitrary, so its action support may vary with history and Assumption 10 is not used. Proof sketch, finite horizon. Both directions turn on one decomposition. Call h(a,o)∈LBπh\,(a,o)∈ L_B_π a first entry when no proper prefix of it lies in LBπL_B_π. When Π(h)>0 (h)>0 every action taken in h lies in AπA_π, so at every step of the prefix of a first entry the two models consult emission rows that agree and LM(h)=LM′(h)L_M(h)=L_M (h). The first entries partition LBπL_B_π into blocks h(a,o′):o′∈O\\,h\,(a,o ):o ∈ O\,\, and because the rows are normalized and the policy factor Π(h)π(h)(a) (h)\,π(h)(a) does not depend on o′o , each block has mass Π(h)π(h)(a)LM(h) (h)\,π(h)(a)\,L_M(h) under either model. Appendix S6.4 derives both directions from it. ∎ The theorem requires normalized emission rows and the action-before-observation ordering, both of which belong to Definition 1 and to the factorization above, and Remark 17 identifies the block decomposition. 5.3 A linear-time decision procedure Corollary 13 (Decision procedure). Under Assumption 10, π-equivalence is decided by reachability in the product automaton. Explore from (q0,q0′)(q_0,q_0 ) along transitions the policy gives positive probability, and at each pair reached test the emission rows of the actions in AπA_π only, reporting equivalence if and only if no pair in BπB_π is reached. This runs in time O(|Q||Q′‖A‖O|)O(|Q|\,|Q |\,|A|\,|O|), linear in the size of the product automaton, and is independent of the horizon. Assumption 10 makes the test at a pair independent of the history that reached it, so one visit settles each pair and the bound does not depend on the horizon. Pec returns a certificate of π-equivalence when no disagreeing pair is reachable and a witness naming the missing experiment when one is. Algorithm S1 in Appendix S1 states it, and the frontier is a queue, so the witness returned has minimum depth. Pec reports that depth as the separating horizon, the length of the shortest separating history, which counts the witness action itself. Pec thereby replaces enumeration over histories, which costs time exponential in the horizon. The witness. When the models are not π-equivalent, the search returns the disagreeing pair it reached together with the action on which the emission rows differ. On the T-maze under a deviation this witness is ((qL,qb),run) (\,(q_L,q_b),\ run\, ), naming runrun in the state pair where the cue model remembers a left cue and the blind model sits in its only state. That is the missing experiment, named without any search over policies, and it is the input to the design problem of §6.2. Validation. On 3700 model pairs, 2500 random and 1200 constructed to be π-equivalent, Pec agreed with a brute-force check that compares the two likelihoods on every policy-supported history up to a fixed horizon. 5.4 Behaviour at scale Figure 1: Cost of deciding identifiability, on log axes. (a) certifying π-equivalence against product size. (b) cost of deciding Assumption 2 of Cipollone et al. (2023) from its definition versus with Pec. The bound of Corollary 13 admits direct measurement. On constructed π-equivalent pairs built from two cycles of coprime length, whose reachable product is exactly |Q|⋅|Q′||Q|·|Q |, Pec explores from 110110 to 1,001,0001,001,000 state pairs at a cost flat to within 8%8\% per pair and a least-squares slope of log(time) (time) against log(pairs) (pairs) of 1.0031.003, plotted in Figure 1(a). A certificate costs the whole reachable product while a witness costs only the part preceding it, so at a product of 1,001,0001,001,000 a witness at depth 999999 returns in 7.2×10−37.2× 10^-3 seconds against 4.654.65 seconds to certify the same instance. Appendix S7.12 reports the full sweeps together with the action-support factor. Definition 11 tests emission rows for exact inequality, whereas estimated tables are built from counts. Two rows estimated from the same distribution then differ with probability approaching one as the corpus grows, so the exact test almost never certifies. Replacing the test by maxo|e(q,a)(o)−e′(q′,a)(o)|>τ _o|e(q,a)(o)-e (q ,a)(o)|>τ for a tolerance τ repairs this. Write η for the sup-norm error of the estimated tables over the rows Pec consults and γ for the smallest sup-norm separation among pairs whose exact rows disagree. Truly equal rows are estimated at most 2η2η apart and truly separated ones at least γ−2ηγ-2η apart, so the tolerant test returns the exact-arithmetic verdict whenever 2η<τ<γ−2η2η<τ<γ-2η, a window non-empty as soon as η<γ/4η<γ/4. Since η shrinks as the corpus grows while γ is a property of the candidates, the window opens at a finite sample size. On the corridor family at 600 trajectories per candidate, η ranges from 0.0720.072 to 0.0980.098 against γ=1/2γ=1/2, and every tolerance inside the window reproduces exact arithmetic (Appendix S7.9). 6 Experiments Code and proofs. The implementation, the synthetic environments, and the Lean 4 development containing the machine-checked proofs are released at https://github.com/Kcbir/pec. Protocol. All environments are synthetic Regular Decision Processes with known ground truth, and all data are simulated. Rotating MAB and Cheat MAB, two multi-armed bandit (MAB) variants, are taken from Abadi and Brafman (2020), and Rotating Maze is a reduced version of the grid-world domain of the same name introduced there, so three of the four come from established benchmarks for this model class. Known ground truth makes the identifiability claims checkable, since a frozen posterior can be verified only against the model the data failed to distinguish. Inference uses exact rational arithmetic throughout, with no sampling and no training, emission parameters being integrated out under a Dirichlet prior to keep the structure posterior rational (Appendix S7.1). Entropy requires a logarithm, so expected information gain alone is computed in floating point, whereas the separating mass of Definition 7 is exact. Scope. A standardized partially observable benchmark such as POPGym (Morad et al., 2023) supplies neither the candidate pair nor the behaviour policy that Pec takes as input. The method requires a known pair whatever the size of the environment, and §5.4 addresses scale directly. 6.1 The distinguishability assumption of RegORL The guarantee of Cipollone et al. (2023) rests on their Assumption 2, that the behaviour policy has L∞pL^p_∞-distinguishability at least μ0>0 _0>0 between every pair of distinct same-layer states of the minimal RDP. Theorem 6 of Cipollone et al. (2023) requires a corpus whose size is proportional to 1/μ01/ _0 (Appendix S7.11), so the requirement diverges as μ0 _0 goes to zero. Table 1 computes that parameter in exact rational arithmetic beside the separating mass of Definition 7. Table 1: Separating mass and the distinguishability parameter of Cipollone et al. (2023) on four environments, as exact rationals, against the verdict Pec returns on the same instance. separating mass μ0 _0 Environment T under π under π′π under π under π′π Assumption 2 Pec T-maze 2 0 1/21/2 0 1/21/2 fails equivalent Rotating MAB 3 0 245/512245/512 0 1/41/4 fails equivalent Cheat MAB 3 0 1/91/9 0 1/241/24 fails equivalent Rotating Maze 4 0 1/81/8 – 9/2569/256 holds (trivially) equivalent On three of the four environments μ0=0 _0=0 as an exact rational, so Assumption 2 fails and the required corpus size diverges. The separating mass is an exact rational zero on each of them, and two of the three are benchmarks from Abadi and Brafman (2020). On Rotating Maze the assumption instead holds trivially, since the behaviour policy reaches a single state per layer and there is no pair of distinct states to compare. The two criteria overlap without either containing the other, because μ0 _0 compares two states of the true model that the policy reaches while π-equivalence compares two candidate models. An ambiguity in a region the policy never enters preserves Assumption 2, as in Rotating Maze, while Pec certifies π-equivalence. Deciding Assumption 2. For a pair of states distinct in the minimal RDP, L∞p>0L^p_∞>0 holds exactly when some π-supported trace prefix within the remaining horizon receives different probability from the two states. By Theorem 12 applied to the sub-automaton started at (q,q′)(q,q ), this is the condition that Pec, started from (q,q′)(q,q ), reports a separating horizon no greater than the number of steps remaining. The definition maximizes over (|A||O|)T(|A|\,|O|)^T trace prefixes at horizon T, whereas Pec explores at most |Q|⋅|Q′||Q|·|Q | pairs without reference to the horizon. On the corridor family of §6.3 the measured ratio grows from 3.73.7 at depth 22 to 67.567.5 at depth 77 (Figure 1(b)), and the two methods agree everywhere (Appendix S7.11). Under the designed deviation μ0 _0 becomes positive in every environment, so the experiment Pec names is the one that restores their assumption. 6.2 Selecting policy deviations Theorem 6 shows that a π-equivalent pair is uncorrectable under π, so the remedy is to change π. We select policy deviations by expected information gain (EIG) under the posterior over the candidate structures, which applies Bayesian active learning by disagreement (BALD) (Houlsby et al., 2011) to automaton structure in a controlled process. Let Mi\M_i\ be the candidate models with prior weights wi\w_i\, and let a candidate experiment be an open-loop action sequence α=(a1,…,ad)α=(a_1,…,a_d), executed by the degenerate policy πα _α that plays ata_t at step t regardless of what it observes. The prior-predictive probability of a history h∈ℋdh _d under πα _α is Pα(h)=Πα(h)∑iwiLMi(h),P_α(h)\;=\; _α(h) _iw_i\,L_M_i(h), where Πα(h)=∏t=1d[ath=at] _α(h)= _t=1^d1[a^h_t=a_t] takes the value 11 on the histories whose actions are α, and the posterior after h is wi(h)∝wiLMi(h)w_i(h) w_iL_M_i(h). The expected information gain of the sequence is EIG(α)=H(wi)−∑h∈ℋdPα(h)>0Pα(h)H(wi(h)),EIG(α)\;=\;H (\w_i\ )\;-\;\!\! _ subarraych _d\\ P_α(h)>0 subarray\!\!P_α(h)\;H (\w_i(h)\ ), with H the Shannon entropy in nats. Greedy design maximizes EIGEIG over the one-step extensions of the sequence built so far, breaking ties by the order in which actions are enumerated, while exhaustive design at lookahead ℓ maximizes it over all |A|ℓ|A| sequences at a cost of O((|A||O|)ℓ)O((|A|\,|O|) ) likelihood computations. Pec returns the required ℓ in linear time, so the depth of that exponential search is known before it is run. Remark 14 (Zero first-step gain). In every environment in our suite, the expected information gain of the first action is exactly zero. In each environment the candidates’ emission rows at their initial states agree on every action, so the separating horizon is at least 22, whereas a pair that disagrees at its initial states would have positive first-step gain. A greedy one-step rule sees equal gain for every first action here, and its tie-break determines what it does. We compare greedy against exhaustive design over sequences whose length equals the separating horizon, running greedy twice with the action order reversed. Table 2: Separating mass achieved by each design rule, as exact rationals. The two greedy columns differ only in the order in which actions are enumerated for the tie-break, and ℓ is the lookahead at which exhaustive design is run. greedy Environment ℓ order reversed exhaustive T-maze 2 11 11 11 Rotating MAB 2 1/21/2 1/41/4 3/43/4 Cheat MAB 3 0 0 11 Rotating Maze 4 0 11 11 Exhaustive design succeeds in every environment, whereas greedy design succeeds on two of the four. Cheat MAB is a structural failure of the greedy rule, since the experiment requires two different actions in sequence and neither action yields any gain alone, so greedy achieves separating mass 00 under both tie-breaks while exhaustive design recovers the unlock sequence (arm1,arm2)(arm1,arm2) from the posterior without being given it. On Rotating Maze the same greedy rule achieves 00 or 11 according to the order in which actions are enumerated, so its success there derives from the tie-break alone, and myopic design is therefore unreliable. 6.3 A parameterized family and the required lookahead The four environments above are fixed, small instances, which leaves open whether the phenomenon survives a controlled change in difficulty. A member of depth d is a corridor of d rooms with the missing experiment placed at the far end. The behaviour policy walks the corridor without probing, and the deviation walks and then probes. The alphabet, the emission values, and the way the two candidates differ stay fixed, and only the corridor length varies, so a curve over the family isolates depth without confounding it with model size or stochasticity. For every member, Pec reports no reachable disagreeing pair under π and reports a separating horizon of exactly d under the deviation (Table S2, Appendix S7.2), so the parameter is read off the structure, with no sweep over horizons. Sweeping the design lookahead ℓ against depth d gives a transition that is exact, since a lookahead below the depth finds nothing while a lookahead equal to it finds the experiment (Table S3, Appendix S7.2). For open-loop search this follows from the definitions, and the sweep confirms it in the implementation, so one structural quantity serves two roles. The separating horizon measures data difficulty, since it ranks the suite in the small-data crossover of Appendix S7.6, and it measures planning difficulty, since it equals the lookahead a designer needs. 6.4 End-to-end evaluation On the four environments of Table 1 the designed experiment does not improve on uniform exploration. Over ten seeds, a corpus gathered under π leaves the log10 _10 Bayes factor at exactly zero in all four environments and on every seed. On three of them the deviation assigns equal probability to every action, so the designed and the random corpus coincide. On Rotating MAB they differ by less than the seed variation, with means and half-ranges of 161.93±20.04161.93± 20.04 and 148.86±17.89148.86± 17.89 (Appendix S7.3). The separating horizons here run from 22 to 44 over 22 or 33 actions, so uniform exploration finds the missing experiment without help. The boundary between the two regimes follows from the structure of the family. To find the missing experiment of a member with separating horizon d, a uniform policy must emit a specific action sequence of length d, namely d−1d-1 steps along the corridor and then the probe, which it does with probability near 2−d2^-d, whereas a designed experiment executes that sequence every time. The advantage therefore grows exponentially in d, which §6.3 identifies as the difficulty axis. Table 3: Mean log10 _10 Bayes factor over 10 seeds by corridor depth, at budgets of 5 and 25 trajectories. budget 5 budget 25 depth d rand. des. ratio rand. des. ratio 2 1.511.51 3.013.01 2.0×2.0× 8.498.49 15.0515.05 1.8×1.8× 4 0.570.57 3.013.01 5.3×5.3× 3.433.43 15.0515.05 4.4×4.4× 6 0.390.39 3.013.01 7.7×7.7× 1.511.51 15.0515.05 10.0×10.0× 8 0.060.06 3.013.01 50.0×50.0× 0.390.39 15.0515.05 38.5×38.5× The designed column does not vary with depth, because the designed experiment reaches the separating history every time, whereas the yield of uniform exploration decays exponentially. Appendix S7.10 repeats the comparison against the access-sequence heuristic that active automata learning libraries ship, which converts the exponential decay into a polynomial one and, at depth eight, narrows the gap in separating mass from a factor of 256256 to a factor of about 88. Which regime a problem occupies is settled by the linear-time detection step, which returns d together with the witness. 7 Limitations The observation set is finite throughout, and continuous observations lie outside every result here. The decision procedure is exact, so on estimated tables it requires the tolerance of §5.4 and holds only inside the window 2η<τ<γ−2η2η<τ<γ-2η, which needs ever larger corpora as the candidates approach equivalence. Exhaustive design remains exponential in the lookahead, and Pec supplies the required depth without reducing that cost. Exact enumeration bounds the hypothesis space at five automaton states. When π is unknown, Pec reads its action support off the corpus, so an action taken too rarely to appear there is treated as never taken. Pec also decides a question about a given pair, and whether a corpus identifies a model within an implicitly specified hypothesis class remains open. 8 Conclusion This paper has addressed whether data collected under a fixed behaviour policy can distinguish two candidate Regular Decision Processes, a question on which existing offline guarantees for this model class depend but which they provide no means to verify. We have shown that π-observationally equivalent candidates leave the posterior odds at the prior odds at every sample size, and that this condition is not implied by state coverage. We have characterized π-equivalence exactly over the disagreeing state–action pairs of the product automaton, whose blame language, unlike the set of histories on which the likelihoods differ, is regular by construction. The characterization yields Pec, which decides equivalence in time linear in the size of the product automaton and, when equivalence fails, names the experiment that the corpus lacks. Applied to the distinguishability assumption of Cipollone et al. (2023), the procedure establishes that the assumption fails on three of our four test environments and that the experiment it names restores the assumption in each case. Extending the analysis to continuous observations and implicitly specified hypothesis classes remains for future work. References Abadi and Brafman (2020) E. Abadi and R. I. Brafman Learning and solving regular decision processes. In Proceedings of the 29th International Joint Conference on Artificial Intelligence (IJCAI), p. 1948–1954. Cited by: §S5.1, §S5.2, §S7.11, §2, §6, §6.1. Abate et al. (2023) A. Abate, Y. Almulla, J. Fox, D. Hyland, and M. Wooldridge Learning task automata for reinforcement learning using hidden Markov models. In Proceedings of the 26th European Conference on Artificial Intelligence (ECAI), Cited by: §S5.1, §2. Berger and Berliner (1986) J. O. Berger and L. M. Berliner Robust Bayes and empirical Bayes analysis with ε -contaminated priors. Annals of Statistics 14 (2), p. 461–486. Cited by: Appendix S3, §S5.5. Berk (1966) R. H. Berk Limiting behavior of posterior distributions when the model is incorrect. Annals of Mathematical Statistics 37 (1), p. 51–58. Cited by: §S6.2, §2. Bhattamishra et al. (2026) S. Bhattamishra, M. Hahn, and V. Kanade Automata learning and identification of the support of language models. In Proceedings of the 14th International Conference on Learning Representations (ICLR), Cited by: §S5.4. Billingsley (1961) P. Billingsley Statistical methods in Markov chains. Annals of Mathematical Statistics 32 (1), p. 12–40. Cited by: §S5.1. Brafman and De Giacomo (2019) R. I. Brafman and G. De Giacomo Regular decision processes: a model for non-Markovian domains. In Proceedings of the 28th International Joint Conference on Artificial Intelligence (IJCAI), Cited by: §S5.1, §1, §2. Cipollone et al. (2023) R. Cipollone, A. Jonsson, A. Ronca, and M. S. Talebi Provably efficient offline reinforcement learning in regular decision processes. In Advances in Neural Information Processing Systems (NeurIPS), Cited by: §S5.1, §S5.2, §S7.11, §S7.11, §1, §1, §2, §2, Figure 1, §6.1, Table 1, §8. Deb et al. (2024) A. Deb, R. Cipollone, A. Jonsson, A. Ronca, and M. S. Talebi Tractable offline learning of regular decision processes. Note: arXiv:2409.02747 Cited by: §S5.1, §S5.2, §2. Deb et al. (2025) A. Deb, R. Cipollone, A. Jonsson, A. Ronca, and M. S. Talebi Offline RL in regular decision processes: sample efficiency via language metrics. In Proceedings of the 13th International Conference on Learning Representations (ICLR), Cited by: §S5.1, §S5.2, §S7.11, §1, §2. Dohmen et al. (2021) T. Dohmen, N. Topper, G. Atia, A. Beckus, A. Trivedi, and A. Velasquez Inferring probabilistic reward machines from non-Markovian reward processes for reinforcement learning. Note: arXiv:2107.04633 Cited by: §S5.3, §2. Fellows et al. (2024) M. Fellows, B. Kaplowitz, C. Schroeder de Witt, and S. Whiteson Bayesian exploration networks. Note: arXiv:2308.13049 Cited by: §S5.5. Ferns et al. (2004) N. Ferns, P. Panangaden, and D. Precup Metrics for finite Markov decision processes. In Proceedings of the 20th Conference on Uncertainty in Artificial Intelligence (UAI), p. 162–169. Cited by: §5.1. Fica and Otop (2025) M. Fica and J. Otop Active automata learning with advice. Note: arXiv:2508.10535 Cited by: §S5.4, §2. Fortz et al. (2026) S. Fortz, F. Ghassemi, L. Henry, F. Howar, T. Neele, J. Rot, and M. Suilen A research agenda for active automata learning. International Journal on Software Tools for Technology Transfer. Note: Special issue of Dagstuhl Seminar 23492. doi:10.1007/s10009-026-00839-z Cited by: §S5.4, §2. Fu et al. (2022) Z. Fu, Z. Qi, Z. Wang, Z. Yang, Y. Xu, and M. R. Kosorok Offline reinforcement learning with instrumental variables in confounded Markov decision processes. Note: arXiv:2209.08666 Cited by: §S5.5, §2. Givan et al. (2003) R. Givan, T. Dean, and M. Greig Equivalence notions and model minimization in Markov decision processes. Artificial Intelligence 147 (1–2), p. 163–223. Cited by: §5.1. Grünwald (2006) P. Grünwald Bayesian inconsistency under misspecification. In Valencia International Meeting on Bayesian Statistics, Cited by: §S5.5. Hopcroft and Karp (1971) J. E. Hopcroft and R. M. Karp A linear algorithm for testing equivalence of finite automata. Technical report Technical Report TR 71-114, Cornell University. Cited by: §5.1. Houlsby et al. (2011) N. Houlsby, F. Huszár, Z. Ghahramani, and M. Lengyel Bayesian active learning for classification and preference learning. Note: arXiv:1112.5745 Cited by: §S5.5, §2, §6.2. Kleijn and van der Vaart (2006) B. J. K. Kleijn and A. W. van der Vaart Misspecification in infinite-dimensional Bayesian statistics. Annals of Statistics 34 (2), p. 837–877. Cited by: §S5.5. Larsen and Skou (1991) K. G. Larsen and A. Skou Bisimulation through probabilistic testing. Information and Computation 94 (1), p. 1–28. Cited by: §5.1. Morad et al. (2023) S. Morad, R. Kortvelesy, M. Bettini, S. Liwicki, and A. Prorok POPGym: benchmarking partially observable reinforcement learning. In Proceedings of the 11th International Conference on Learning Representations (ICLR), Cited by: §6. Muskardin et al. (2022) E. Muskardin, B. K. Aichernig, I. Pill, A. Pferscher, and M. Tappler AALpy: an active automata learning library. Innovations in Systems and Software Engineering 18, p. 417–426. Cited by: §S5.4, §S7.10, §2. Parbhoo et al. (2022) S. Parbhoo, S. Joshi, and F. Doshi-Velez Generalizing off-policy evaluation from a causal perspective for sequential decision-making. Note: arXiv:2201.08262 Cited by: §S5.5, §2. Pethel and Hahs (2013) S. D. Pethel and D. W. Hahs Exact test for Markov order. Note: arXiv:1302.1500 Cited by: §S5.1. Pfau et al. (2010) D. Pfau, N. Bartlett, and F. Wood Probabilistic deterministic infinite automata. In Advances in Neural Information Processing Systems (NIPS), Cited by: §S5.3, §2. Rens et al. (2020) G. Rens, J.-F. Raskin, R. Reynouad, and G. Marra Online learning of non-Markovian reward models. Note: arXiv:2009.12600 Cited by: §S5.1, §2. Ronca et al. (2023) A. Ronca, N. A. Knorozova, and G. De Giacomo Automata cascades: expressivity and sample complexity. In Proceedings of the 37th AAAI Conference on Artificial Intelligence, Cited by: §S5.1, §2. Ronca et al. (2022) A. Ronca, G. P. Licks, and G. De Giacomo Markov abstractions for PAC reinforcement learning in non-Markov decision processes. In Proceedings of the 31st International Joint Conference on Artificial Intelligence (IJCAI), Cited by: §S5.1, §2. Ross et al. (2011) S. Ross, J. Pineau, B. Chaib-draa, and P. Kreitmann A Bayesian approach for learning and planning in partially observable Markov decision processes. Journal of Machine Learning Research 12, p. 1729–1770. Cited by: §S5.5. Shalizi (2009) C. R. Shalizi Dynamics of Bayesian updating with dependent data and misspecified models. Electronic Journal of Statistics 3, p. 1039–1074. Cited by: §S5.5, §S6.2, §2. Shibata and Yoshinaka (2014) C. Shibata and R. Yoshinaka A comparison of collapsed Bayesian methods for probabilistic finite automata. Machine Learning 96 (1–2), p. 155–188. Cited by: §S5.3, §2. Takahashi (2026) T. Takahashi Why conclusions diverge from the same observations: formalizing world-model non-identifiability via an inference. Note: arXiv:2605.12255 Cited by: §S5.5, §2. Tappler et al. (2021) M. Tappler, B. K. Aichernig, G. Bacci, M. Eichlseder, and K. G. Larsen L∗L^*-based learning of Markov decision processes. Formal Aspects of Computing 33, p. 575–615. Note: Extended version: arXiv:1906.12239 Cited by: §S5.4, §S5.4, §2. Topper et al. (2024) N. Topper, A. Velasquez, and G. Atia Bayesian inverse reinforcement learning for non-Markovian rewards. Note: arXiv:2406.13991 Cited by: §S5.3, §2. Toro Icarte et al. (2022) R. Toro Icarte, T. Q. Klassen, R. Valenzano, and S. A. McIlraith Reward machines: exploiting reward function structure in reinforcement learning. Journal of Artificial Intelligence Research 73, p. 173–208. Cited by: §S5.1, §2. Umili and Capobianco (2024) E. Umili and R. Capobianco DeepDFA: automata learning through neural probabilistic relaxations. Note: arXiv:2408.08622 Cited by: §S5.3, §2. Varricchione et al. (2025) G. Varricchione, T. Q. Klassen, N. Alechina, M. Dastani, B. Logan, and S. A. McIlraith Pushdown reward machines for reinforcement learning. In Proceedings of the 22nd International Conference on Principles of Knowledge Representation and Reasoning (KR), Cited by: §S5.1, §2. Zhu et al. (2026) Z. Zhu, Z. Chen, C. Zhu, M. Li, W. Zhang, and F. Wang Noise-robust reward machine induction via probabilistic modeling and genetic local search. Scientific Reports 16, p. 27091. Cited by: §S5.3, §2. Exact Distinguishability in Non-Markovian Decision Processes: Supplementary Materials Appendix S1 The decision procedure Algorithm S1 states Pec, the procedure of §5.3. It explores the product automaton within the support of the behaviour policy and halts at the first disagreeing pair. A returned witness names the missing experiment, and a returned ⊥ certifies π-equivalence at every horizon. Algorithm S1 Pec: decide π-equivalence and return a witness. 1: models M=(Q,q0,δ,e)M=(Q,q_0,δ,e) and M′=(Q′,q0′,δ′,e′)M =(Q ,q_0 ,δ ,e ), behaviour policy π 2: a pair ((q,q′),a)((q,q ),a) naming the missing experiment, or ⊥ if M∼πM′M _πM 3: Aπ←a∈A:π(λ)(a)>0A_π←\\,a∈ A:π(λ)(a)>0\,\ ⊳ action support, history-independent by assumption 4: s0←(q0,q0′)s_0←(q_0,q_0 ); S←s0S←\s_0\; F←F← queue holding s0s_0 5: while F≠∅F≠ do 6: dequeue (q,q′)(q,q ) from F 7: for all a∈Aπa∈ A_π do 8: if ∃o∈O∃\,o∈ O with e(q,a)(o)≠e′(q′,a)(o)e(q,a)(o)≠ e (q ,a)(o) then 9: return ((q,q′),a)((q,q ),a) ⊳ reachable disagreeing pair 10: end if 11: end for 12: for all a∈Aπa∈ A_π and o∈Oo∈ O with e(q,a)(o)>0e(q,a)(o)>0 do 13: s←(δ(q,a,o),δ′(q′,a,o))s← (δ(q,a,o),\,δ (q ,a,o) ) 14: if s∉Ss∉ S then 15: S←S∪sS← S∪\s\; enqueue s on F 16: end if 17: end for 18: end while 19: return ⊥ ⊳ no disagreeing pair reachable Each state pair enters S at most once, and the work at a state is O(|A||O|)O(|A|\,|O|), so Pec runs in time O(|Q||Q′‖A‖O|)O(|Q|\,|Q |\,|A|\,|O|) and uses O(|Q||Q′|)O(|Q|\,|Q |) space. Recording the level at which the loop returns gives the minimum separating horizon, which is the depth reported in Table S2 and the lookahead required in Table S3. Two details of the frontier determine which experiment is returned and what it costs. The disagreement test runs as each pair is dequeued, before the reachable set is complete, so a witness costs only the part of the product that precedes it (Appendix S7.12 measures this), while a certificate costs the whole of it. Because F is a queue, pairs are visited in order of distance from (q0,q0′)(q_0,q_0 ), so the witness returned has minimum depth and is the same on every run. An implementation that instead scans the reachable set as an unordered collection returns an equally valid witness that depends on the iteration order of that collection, and on the T-maze it names qLq_L or qRq_R accordingly. Pec probes the action support of π at the empty history, which is exact under Assumption 10 (Remark 18). A policy whose support varies with history requires folding the support into the product automaton, which enlarges the automaton without changing the argument. This extension limits the scope of the procedure as well as its cost. Folding is available only when the support is a regular function of history, that is, when some finite automaton with state set QπQ_π reads the action–observation sequence and determines AπA_π from its state. The search then runs over Q×Q′×QπQ× Q × Q_π, and the two bounds above pick up a factor of |Qπ||Q_π|, giving O(|Q‖Q′‖Qπ‖A‖O|)O(|Q|\,|Q |\,|Q_π|\,|A|\,|O|) time and O(|Q‖Q′‖Qπ|)O(|Q|\,|Q |\,|Q_π|) space, still with no horizon. If the support is an arbitrary function of history the folded automaton is infinite, reachability over it is not a finite computation, and Pec does not apply. Regularity of the policy’s support is therefore the outer limit of the method. Appendix S2 The T-maze construction Figure S1 displays the two hypotheses of §4.1. The cue model McueM_cue records the first observation and never revises it, whereas the blind model MblindM_blind has a single state. They differ only in what the action runrun emits, and runrun is the action the behaviour policy never takes. Over histories of length two, the support of the behaviour policy and the set on which the two likelihoods disagree are therefore disjoint, which is the π-equivalence asserted in Proposition 8. Each of the two cue-tracking states is visited with probability exactly 1/21/2 under the behaviour policy, which is the coverage fact recorded in the same proposition. Figure S1: The two hypotheses of the T-maze construction. Edges carry the action–observation pair that drives them, as in Definition 1, with ∗ standing for any element of the alphabet in that slot. Neither transition function consults the action, so every edge is labelled ∗ there, and the (∗,∗)( , ) self-loops on qLq_L, qRq_R and qbq_b are the ones the always-waitwait policy traverses. Appendix S3 Value of a structural description A structural description can also enter as a prior. We encode a sentence by hand as a predicate on transition structures and take the prior ρL _L uniform on the structures it admits, contaminated towards an uninformative prior ρ0 _0 at rate ε , giving (1−ε)ρL+ερ0(1- ) _L+ \, _0 (Berger and Berliner, 1986). The hypothesis space is every transition structure on at most three states over the T-maze observations, one per state-renaming class, 229229 in all, and ρ0 _0 is uniform over it. Three sentences of increasing specificity admit 179179, 1919, and 11 of these structures. The vague sentence, “history matters”, requires the first observation to lead to different states. The partial sentence, “remembers, commits”, also requires one of those states to be absorbing, and the saturated sentence requires both to be, which pins the truth and so amounts to a specification of the model. The wrong description of panel 2(c) is the negation of the vague one. Panel 2(a) shows posterior contraction towards the true model under priors of increasing specificity, where the gap opens in the small-data regime and closes as data accumulate. Panel 2(b) states the same fact as a ratio against the uninformative prior, for the partial sentence alone, which is the 19/22919/229 curve of panel 2(a) divided by the no-sentence baseline. Panel 2(c) covers misspecification, where a wrong description at ε=0 =0 places zero prior mass on the truth and the posterior never reaches it, while any ε>0 >0 recovers it. (a) Posterior contraction. (b) Gain from the partial sentence. (c) A wrong description. Figure S2: Effect of description specificity and of misspecification on the posterior. Panel (a) plots all three sentences against the no-sentence baseline. Panel (b) plots the partial sentence “remembers, commits” alone, named on the axes, since the vague sentence is worth 1.3×1.3× at its peak and the saturated one is a specification. Appendix S4 Seed variation and prior sensitivity Figure S3 plots the seed variation, prior sensitivity and small-data crossover reported in Appendix S7.6. Panel 3(a) shows the mean and range of the log10 _10 Bayes factor over 12 seeds, panel 3(b) the sweep over the Dirichlet concentration, and panel 3(c) the number of seeds that favour the memoryless null as the number of trajectories grows. (a) Variation over 12 seeds. (b) Dirichlet concentration sweep. (c) Small-data crossover. Figure S3: Seed variation, prior sensitivity, and the small-data crossover. Appendix S5 Extended Related Work S5.1 Non-Markovian formalisms Table S1: Location of history-dependence across non-Markovian formalisms. MDP: Markov decision process; POMDP: partially observable MDP; PSR: predictive state representation. Formalism History-dependence in Notes Reward machines reward only dynamics stay Markov; mature literature Regular Decision Processes dynamics and reward more general; less studied MDP (incl. LMDP∗L^*_MDP setting) none, state is Markov structure learning ≠ non-Markovian dynamics POMDP latent state more general, much less tractable PSR / spectral predictive state learning-theoretic, different toolchain Toro Icarte et al. (2022) give the standard reference for reward machines, where recent work has extended expressiveness through pushdown reward machines (Varricchione et al., 2025) and through neural and visual variants. Our question instead concerns identifiability from data. Brafman and De Giacomo (2019) introduced Regular Decision Processes, and Abadi and Brafman (2020) gave the first method for learning and solving them. Later learning results are offline reinforcement learning with PAC guarantees (Cipollone et al., 2023; Deb et al., 2025; Deb et al., 2024), alongside Markov abstractions for PAC reinforcement learning in non-Markov decision processes (Ronca et al., 2022), online learning of non-Markovian reward models (Rens et al., 2020), learning task automata through hidden Markov models (Abate et al., 2023), and automata cascades (Ronca et al., 2023). None of this work uses priors or side information. Markov-order testing goes back to Billingsley (1961), with modern order tests based on conditional mutual information and an exact test using surrogate data (Pethel and Hahs, 2013), none of which handles actions and a behaviour policy. S5.2 Offline learning in Regular Decision Processes Cipollone et al. (2023) give the first provably efficient offline reinforcement learning framework for Regular Decision Processes. The method learns an automaton-based abstraction from a fixed corpus and then runs an offline algorithm over the resulting Markov model, and its PAC bound is stated relative to a distinguishability quantity together with a concentrability condition on the behaviour policy. Deb et al. (2024) and Deb et al. (2025) continue that line, the latter replacing the L∞pL_∞^p-distinguishability parameter with a formal-language metric because the original quantity decays exponentially in the number of automaton states, which is the reason we discuss that parameter in §1. RegORL and this paper divide the labour between them, so a head-to-head comparison would not be meaningful. RegORL returns a policy together with a suboptimality bound that is conditional on the corpus being distinguishing. It does not decide whether that condition holds, and the corpus alone cannot decide it, because the condition concerns models that the corpus fails to separate, whereas Pec decides it from the candidate models (§6.1). The two methods therefore return objects that are not commensurable as estimators, and they are related through the parameter itself. Their μ0 _0 is a property of the true RDP and the policy together, obtained by comparing the suffix distributions of two states the policy reaches, whereas Pec compares two candidate models. Appendix S7.11 computes μ0 _0 on all four environments. On three of them it is exactly zero, so Assumption 2 fails and the bound is vacuous, and on each of them Table 1 also reports a rational zero for the separating mass. Two of these three environments are taken from Abadi and Brafman (2020). On Rotating Maze, and on the whole corridor family, the assumption is instead satisfied trivially, since the policy reaches a single state per layer and there is no pair of distinct states to compare. The parameter does not flag those instances, while Pec certifies π-equivalence on every one of them, so does not vanish on every instance our criterion flags. S5.3 Bayesian inference over automata and reward machines Bayesian inference over automata exists, but it stands apart from decision processes. Probabilistic Deterministic Infinite Automata (Pfau et al., 2010) give a nonparametric Bayesian prior over probabilistic deterministic finite automata, with Markov chain Monte Carlo (MCMC) over an infinite mixture that averages over state cardinality. The uninformative baseline ρ0 _0 of Appendix S3 is simpler, a uniform prior over the transition structures with at most three states. Collapsed Gibbs and collapsed variational methods for probabilistic finite automata (Shibata and Yoshinaka, 2014) marginalize transition probabilities, and DeepDFA (Umili and Capobianco, 2024) learns automata through neural probabilistic relaxations. Bayesian treatments of non-Markovian rewards sit closer to control but still place the history-dependence in the reward alone. Bayesian inverse reinforcement learning for non-Markovian rewards (Topper et al., 2024) infers reward machines from expert behaviour without identifiability or contraction guarantees, and related work infers probabilistic reward machines from non-Markovian reward processes (Dohmen et al., 2021). Closest in spirit is PI-GLS (Zhu et al., 2026), which performs noise-robust reward machine induction with Bayesian handling of uncertain labels and belief-aware shaping over distributions on reward machine states. S5.4 Active automata learning LMDP∗L^*_MDP. The nearest prior art is Tappler et al. (2021), who learn complete MDP structure, including states, from black-box interaction. They use schedulers, their term for behaviour policies, computed to maximize the reachability of a target state, so they already design policies to disambiguate, and they answer equivalence queries by directed testing. Their setting is a Markov MDP, whose semantics map test sequences to output distributions under Myhill–Nerode equivalence over traces, and the object recovered is the state structure of a process that is Markov given the state. LMDP∗L^*_MDP does not require an omniscient teacher, since its equivalence queries are answered by directed testing, and the implementations that ship with AALpy (Muskardin et al., 2022) answer them statistically, through a random walk with a reset probability or through replaying an access sequence to a hypothesis state and continuing at random. These are sound approximations. The setting of LMDP∗L^*_MDP differs from ours in three respects. An equivalence test of any accuracy must issue new traces against a live system, whereas our input is a fixed corpus that cannot be extended. Section 6.2 makes the comparison quantitative, §S7.10 scores the two AALpy strategies directly, and §S7.7 states the limits of the claim. Advice and supervision. Fica and Otop (2025) use advice in the form of a string rewriting system, which is a deductive hard constraint derived from system properties such as idempotence and commutativity. Their setting has no Bayesian framework, no posterior, and no identifiability analysis, so it is the deductive counterpart to the probabilistic approach taken here. Bhattamishra et al. (2026) prove that the class of automata with at most n states is identifiable from positive examples together with next-symbol-prediction labels, and they give the Lnsp∗L^*_nsp algorithm. Their notion of identifiability concerns labels on sequences, with no actions, no behaviour policy, and no dynamics, whereas ours is relative to a policy. Research agenda. Fortz et al. (2026) give a research agenda for active automata learning arising from Dagstuhl Seminar 23492. Its framing assumes a minimally adequate teacher throughout, and it does not treat Bayesian methods, identifiability, non-Markovian dynamics, side information, or prior knowledge. Its §6.1 names the gap in our nearest prior art. The probabilities in the MDPs of Tappler et al. (2021) come from maximum likelihood estimates, that is, fractions of observation counts, and do not account for statistical error through confidence intervals. The agenda proposes to close that gap in the frequentist way, investigating in its Challenge 27 whether approximate automata learning techniques with PAC guarantees are possible for quantitative systems. S5.5 Non-identifiability, misspecification, and experimental design The freezing mechanism is known in off-policy evaluation and in causal identification. In off-policy evaluation, Parbhoo et al. (2022) show that under partial observability the estimate is unavailable even with infinite observational data from the behaviour policy, and Takahashi (2026) and Fu et al. (2022) study related non-identifiability in world models and in confounded Markov decision processes. In causal identification under Markov equivalence, observational equivalence is close to definitional. Our setting is not subsumed by these, because in a Markov MDP non-identifiability under a behaviour policy is a coverage condition on the state–action pairs of the true model, whereas in a Regular Decision Process it is a coverage condition on the product of the two candidates, and §4.1 shows that covering every state of the true model does not suffice. The supporting theory is classical. Berger and Berliner (1986) introduced ε -contaminated priors, which mix an elicited prior with weight 1−ε1- and a contaminating distribution with weight ε , and Kleijn and van der Vaart (2006) give rates under misspecification through a martingale identity. Shalizi (2009) matters most here, because reinforcement learning trajectories are dependent data, and it gives sufficient conditions for posterior convergence when every hypothesis is wrong and the data are dependent. Grünwald (2006) shows that Bayesian inference can be inconsistent under misspecification. Work on ε -contamination addresses continuous parameter spaces, and we found no treatment of contraction over discrete structured spaces, so we use it as machinery in Appendix S3. Posterior sampling, Bayes-adaptive MDPs, Bayesian Exploration Networks (Fellows et al., 2024), and Ross et al. (2011) maintain a posterior over models and solve the exploration–exploitation trade-off in a Bayes-optimal way, always over parameters of Markov MDPs. BALD (Houlsby et al., 2011) and Bayesian experimental design select queries by expected information gain and are mature for classification and regression. We found no prior work combining Bayesian priors over automaton structure with information-gain query selection, and §6.2 gives our instantiation of that combination. Appendix S6 Additional Theory S6.1 Formalization and the nonzero-likelihood hypothesis Theorem 6 is formalised in Lean 4 against Mathlib. The development proves the odds identity, the statement that the odds stay fixed at every sample size, the corresponding statements for the normalized posterior, and the corollary for global equivalence. It contains no incomplete proofs, and an axiom audit confirms that every theorem depends only on propositional extensionality, the axiom of choice, and the soundness of quotients. The nonzero-likelihood hypothesis. Theorem 6 requires LM′(h)≠0L_M (h)≠ 0, and the requirement is easy to overlook, because division in [0,∞][0,∞] is total and the ratio is therefore never ill-formed. Totality of the operation does not suffice here. Where both likelihoods vanish the odds become 0/0=00/0=0, which need not equal w/w′w/w , so the identity holds only where the hypothesis does. The hypothesis is natural on its own terms. A history that both models assign probability zero cannot be observed under either hypothesis, so it carries no evidence and says nothing about how the odds move. Finiteness needs no such hypothesis, since likelihoods are products of probabilities and so are at most 11, which we also prove. Two observations about the formalisation: 1. Mathlib supports non-Markovian dynamics directly. One might expect the construction of the trajectory measure to dominate the cost in Lean. The trajectory construction in Mathlib takes, at each step n, a kernel κn _n from ∏i≤nXi _i≤ nX_i to Xn+1X_n+1, so each step’s kernel already conditions on the entire history and X may vary with the timestep. History-dependence is the native shape of the Ionescu–Tulcea interface, so a Regular Decision Process under a fixed π is a direct instance of it. The definitional cost lies instead in the automaton-indexed kernel and the posterior bookkeeping. 2. Theorem 6 needs no measure theory. It is finite-horizon and combinatorial, since equal per-history likelihoods give equal posterior odds, so formalising it over finite lists of action–observation pairs keeps the proof short. The same holds for most of the martingale development, as §S6.2 describes. S6.2 Conservation of posterior weight The posterior over a fixed pair of hypotheses is a bounded martingale with respect to the data filtration, and so converges almost surely by Doob’s theorem. We separate the combinatorial part of that statement from the part that requires a measure space, because the two carry different costs in a proof assistant and the combinatorial part carries the substance of the argument. Proposition 15 (Conservation of posterior weight). For any prior weight w, model M, history h and action a, ∑o∈OwLM(h(a,o))=wLM(h), _o∈ Ow\,L_M (h\,(a,o) )\;=\;w\,L_M(h), and the same identity holds for the evidence wLM(h)+w′LM′(h)w\,L_M(h)+w \,L_M (h). Consequently the normalized posterior satisfies the one-step tower property, and lies in [0,1][0,1]. Summing posterior weight over the next observation returns the previous weight, which is the martingale property in combinatorial form. We prove it in Lean over finite histories, along with the one-step likelihood decomposition, the lifted statement that emission rows sum to one, conservation of the evidence, the bound placing the posterior in [0,1][0,1], and the one-step tower property. The proof uses no measure space, no Ionescu–Tulcea construction, and no filtration. The identity concerns finite sums over O, and it holds because emission rows are normalized. Scope of the claim. The statement of almost-sure convergence still requires the trajectory measure. Proposition 15 establishes that every hypothesis Doob’s theorem requires holds, since the process is adapted, bounded in [0,1][0,1], and satisfies the tower property. The remaining step is the construction of the measure, and it involves no further combinatorial content. We quote the consequences from the literature. When the truth is among the hypotheses and identifiable under π, the posterior concentrates on it, and when every hypothesis is wrong, it concentrates on the hypotheses closest to the truth in Kullback–Leibler divergence (Berk, 1966; Shalizi, 2009). Between hypotheses that are π-equivalent, Theorem 6 keeps the posterior odds at their prior values. S6.3 Structural account In a Markov MDP the model factorizes into conditionals indexed by (s,a)(s,a), so covering every such pair identifies every parameter. In a Regular Decision Process the automaton state is unobservable, being a deterministic function of history, so identification depends on which combinations of history pattern and action occur. A policy can cover every state while avoiding the joint pattern that separates the hypotheses. The always-wait policy reaches the relevant state but never takes the action that exposes the difference there. Remark 16 (Two actions are necessary). A one-action variant of this construction cannot exhibit the phenomenon. With a single action the policy makes no choice, so it cannot leave any experiment missing. Taking one action with an emission that is deterministic after the cue does not repair this, since the two models then disagree on consistent histories of length at least 22, with likelihoods 1/21/2 and 1/41/4, so no policy renders them equivalent. S6.4 Proof of Theorem 12 We complete the argument sketched in §5, retaining the notation of that section. Recall that the first entries partition LBπL_B_π into blocks h(a,o′):o′∈O\\,h\,(a,o ):o ∈ O\,\, each of mass Π(h)π(h)(a)LM(h) (h)\,π(h)(a)\,L_M(h) under either model. Suppose first that ℙπ(LBπ)>0P^π(L_B_π)>0. Some block then has positive mass, so Π(h)π(h)(a)>0 (h)\,π(h)(a)>0 and LM(h)=LM′(h)>0L_M(h)=L_M (h)>0. Writing (q,q′)=Δ^(h)(q,q )= (h) and taking o to be an observation witnessing ((q,q′),a)∈Bπ((q,q ),a)∈ B_π, LM(h(a,o))=LM(h)e(q,a)(o)≠LM′(h)e′(q′,a)(o)=LM′(h(a,o))L_M(h\,(a,o))=L_M(h)\,e(q,a)(o)≠ L_M (h)\,e (q ,a)(o)=L_M (h\,(a,o)) on a history the policy generates with positive probability, so M≁πM′M _πM . Suppose conversely that M≁πM′M _πM , and let h(a,o)h\,(a,o) be a shortest history of positive policy probability on which the two likelihoods differ. Minimality gives LM(h)=LM′(h)L_M(h)=L_M (h), and that common value is nonzero, since otherwise both extensions would vanish as well and the likelihoods would agree on h(a,o)h\,(a,o). Dividing through by it yields e(q,a)(o)≠e′(q′,a)(o)e(q,a)(o)≠ e (q ,a)(o), so ((q,q′),a)∈Bπ((q,q ),a)∈ B_π, and a∈Aπa∈ A_π because Π(h(a,o))>0 (h\,(a,o))>0. The whole block over h and a therefore lies in LBπL_B_π and carries mass Π(h)π(h)(a)LM(h)>0 (h)\,π(h)(a)\,L_M(h)>0, whence ℙπ(LBπ)>0P^π(L_B_π)>0. The infinite-horizon statement follows from Proposition 19. ∎ S6.5 Scope conditions for the criterion Rewards as observations. Definition 1 carries no separate reward function, while §1 motivates the setting by offline reinforcement learning corpora, so we state the correspondence. An RDP whose reward is a history-dependent random variable taking finitely many values is the case O=Oenv×RO=O_env× R for a finite reward set R, with e(q,a)e(q,a) the joint emission over the observed pair, and a reward that is a deterministic function of (q,a,o)(q,a,o) requires no product at all. Two of our environments are of the first form, since Rotating MAB and Cheat MAB observe the reward and nothing else. Everything in §5 concerns e alone and so applies unchanged once the reward is read as a component of the observation. Folding it in makes ∼π _π the finer relation, since two models that agree on the environment observation while differing in reward contribute a disagreeing pair to the criterion and are separable exactly when the behaviour policy exercises that pair. The finiteness of R is the same finite-alphabet assumption we make of O throughout, so continuous rewards fall outside the scope of these results. Restriction of the quantifier to AπA_π. Dropping the restriction to the actions the policy can take would place Corollary 13 in contradiction with Proposition 8. Under the always-waitwait policy the T-maze reaches one of the state pairs (qL,qb)(q_L,q_b) and (qR,qb)(q_R,q_b) with probability one, and at both the two emission rows differ under runrun. Collecting disagreeing pairs over all of A and then testing membership by reaching such a pair would therefore declare the two models distinguishable, whereas Proposition 8, proved in Lean, establishes that they are π-equivalent, so the posterior never moves. Since run∉Aπrun∉ A_π the pairs do not enter BπB_π, the procedure reports equivalence, and ℙπ(LBπ)=0P^π(L_B_π)=0 as Theorem 12 requires. The trailing action. Requiring the history to take the witnessing action at the pair, in addition to reaching it, is a sharpening independent of the restriction to AπA_π. Carrying the action makes ℙπ(LBπ)P^π(L_B_π) weight every candidate blame step by π(h)(a)π(h)(a), which is why Theorem 12 needs neither Assumption 10 nor the restriction of BπB_π to AπA_π, since an action the policy never takes contributes no mass on its own. Under Assumption 10 the two readings coincide, because if a∈Aπa∈ A_π and the product automaton reaches (q,q′)(q,q ) after a history of positive probability then the policy takes a there with positive probability, so reaching the pair and exercising it there have the same null sets. That coincidence permits Algorithm S1 to test the pair alone. A policy whose support varies with history separates the two readings, and the reading with the trailing action is the one that remains correct. Remark 17 (The two hypotheses the theorem requires). Theorem 12 requires normalized emission rows and the ordering in which the action precedes the observation. Normalization collapses the sum over o′o within a first-entry block to the mass of its prefix, and the action-before-observation ordering keeps the policy factor Π(h)π(h)(a) (h)\,π(h)(a) outside that sum, so that no policy can shift mass between the two models at the blame step. Both belong to Definition 1 and to the factorization in §3. A formalism with simultaneous action and observation timing therefore requires a check of this correspondence, since dropping either hypothesis breaks the argument. Ambiguity of the measure. The phrase “measure zero under ℙπP^π” would be ambiguous over an arbitrary set of histories, since a history that M calls impossible may be one that M′M allows, and such a history has M-measure zero while witnessing that the models are not π-equivalent. Over LBπL_B_π the ambiguity does not arise, because every first-entry block carries the same mass Π(h)π(h)(a)LM(h)=Π(h)π(h)(a)LM′(h) (h)\,π(h)(a)\,L_M(h)= (h)\,π(h)(a)\,L_M (h) under both models, so ℙMπ(LBπ)=ℙM′π(LBπ)P^π_M(L_B_π)=P^π_M (L_B_π) and the subscript may be dropped. The disagreement set of §S6.6 has neither property, and the compensating-history argument that removes the ambiguity there is given in that section. Remark 18 (A caveat on the policy). Definition 9 quantifies AπA_π over every history the policy can generate, whereas the implementation probes the support at the empty history alone. The two agree exactly when the action support does not vary with history, which holds for every policy in our suite, and we verify it over all histories up to a fixed length. A policy whose support varies requires folding the support into the product automaton, which Appendix S1 describes together with the regularity condition it needs and its cost. S6.6 The conjecture over the disagreement set The natural conjecture concerns the disagreement set D(M,M′)=h∈ℋ:LM(h)≠LM′(h),D(M,M )\;=\;\\,h \;:\;L_M(h)≠ L_M (h)\,\, and it asserts that M∼πM′M _πM iff ℙπ(D)=0P^π(D)=0. Treating D as tractable would require it to be regular, and a product construction on the two automata appears to show that it is. The product construction does not establish this, because LM(h)L_M(h) is a product of real numbers. Two histories that drive the product automaton into unrelated state pairs can still have equal likelihoods by arithmetic coincidence, as when a factor of 12⋅23 12· 23 on one path matches 13⋅1 13· 1 on another. Membership in D therefore depends on the numerical value of a product, which no finite-state property of h determines, so in general no finite automaton recognizes it. The product construction proves the regularity of a different set from the one D names. The coinciding parameter values are not pathological, since nothing distinguishes them from any others. Readings of the conjecture. The biconditional the conjecture asserts is true. The phrase ℙπ(D)=0P^π(D)=0 admits three readings, namely (A) ℙMπ(D)=0P^π_M(D)=0, (B) ℙMπ(D)=0P^π_M(D)=0 and ℙM′π(D)=0P^π_M (D)=0 together, and (C) π-equivalence itself. At finite horizon all three coincide, so the conjecture holds under each. That (B) implies (C) is immediate. That the weaker reading (A) implies it as well is the content of the compensating-history argument, which runs as follows. Let h(a,o)h\,(a,o) be a shortest history of positive policy probability on which the likelihoods differ, so that LM(h)=LM′(h)≠0L_M(h)=L_M (h)≠ 0 and the two emission rows at Δ^(h)=(q,q′) (h)=(q,q ) differ under a. Those rows are normalized, so some o′o has e(q,a)(o′)>e′(q′,a)(o′)≥0e(q,a)(o )>e (q ,a)(o )≥ 0 and in particular e(q,a)(o′)>0e(q,a)(o )>0. The compensating history h(a,o′)h\,(a,o ) then lies in D and carries positive M-mass, and because the policy picks a before seeing that step’s observation the factor Π(h)π(h)(a) (h)\,π(h)(a) is common to both models, so no policy can suppress it. We checked this on 4500 model pairs, 3000 random and 1500 constructed to be π-equivalent, and the three readings agreed on every pair. We also checked the compensating-history argument itself, confirming that the intended witness lies in D with zero mass while the compensating history lies in D with positive mass, as the argument requires. The conjecture is therefore true but of no use for deciding equivalence. Because D is not regular, the conjecture concerns an object with no finite-state description, so it certifies nothing about a given pair, yields no decision procedure, and cannot be carried to infinite horizon through the regularity of D. The null-set arguments that such an extension appears to require arise from the choice of object. Section 5 therefore changes the object, asking the same question of LBπL_B_π, which is regular by construction, and Proposition 19 then settles infinite horizon by countable additivity alone. S6.7 Extension to infinite horizon The infinite-horizon case requires no separate treatment of null sets under the trajectory measure. Proposition 19 (Infinite horizon). Write EBπE_B_π for the event that some prefix of an infinite trajectory lies in LBπL_B_π. Then EBπ=⋃h∈LBπminCyl(h)E_B_π= _h∈ L_B_π Cyl(h), where LBπminL_B_π is the countable set of first entries of LBπL_B_π. Hence ℙπ(EBπ)=0P^π(E_B_π)=0 iff ℙπ(Cyl(h))=0P^π(Cyl(h))=0 for every such h, by countable additivity alone. Beyond the existence of the trajectory measure, which the Ionescu–Tulcea construction provides, the argument needs neither a martingale argument nor a regularity condition on the disagreement set. The restatement in Definition 11 makes this possible, since it replaces a set defined by arithmetic with one defined by reachability. Appendix S7 Additional Experimental Results S7.1 The two inference paths This paper uses two likelihoods, which serve different results. Fixed emissions, exact. The identifiability and design results take a pair of fully specified candidates whose emission tables are given rationals. The likelihood is LM(h)L_M(h) of Definition 2, the posterior over the pair is the normalized product of prior and likelihood, and nothing is integrated out. This path produces the separating masses of Definition 7, the expected information gains of §6.2, and the log Bayes factors of Table S4 and Table 3. Integrated emissions, Dirichlet. The structure-level results take the emissions to be unknown and the transition function to be the object of inference. Placing an independent symmetric Dirichlet(α)Dirichlet(α) prior on each emission row and integrating gives, for a corpus x with counts nq,a(o)n_q,a(o) of observation o at the pair (q,a)(q,a) and Nq,a=∑onq,a(o)N_q,a= _on_q,a(o), P(x∣δ)=∏(q,a)(kα−1)!((α−1)!)k⋅∏o∈O(nq,a(o)+α−1)!(Nq,a+kα−1)!,k=|O|,P(x δ)\;=\; _(q,a) (kα-1)! ((α-1)! )^k· _o∈ O (n_q,a(o)+α-1 )! (N_q,a+kα-1 )!, k=|O|, which for integer α is a ratio of factorials and so an exact rational, keeping the structure posterior rational. We use α=1α=1 throughout and sweep it over 1,2,3,5,10\1,2,3,5,10\ in §S7.6. This path produces the Bayes factors against a memoryless null in Table S5, the Tomita panel of Figure S4, and the priors of Appendix S3. Where a point estimate of an emission row is needed, as in Table S6, it is the posterior mean (nq,a(o)+α)/(Nq,a+kα) (n_q,a(o)+α )/ (N_q,a+kα ) under the same prior. The design objective of §6.2 is stated over the first path, because the question Pec decides concerns a given pair of candidates. Which structure a corpus supports is the question of the second path, and only the results listed above use it. S7.2 Structural depth in the corridor family Table S2 reports the separating horizon that Pec measures for each member of the family of §6.3, against the depth the member was built to have. Table S2: Corridor depth against the measured separating horizon. A horizon of ⊥ means that Pec found no reachable disagreeing pair, so no finite horizon separates the two models and the entry is a certificate of π-equivalence. requested depth 1 2 3 4 5 6 8 rooms 1 2 3 4 5 6 8 π-equivalent yes yes yes yes yes yes yes horizon under π ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ horizon under deviation 1 2 3 4 5 6 8 Table S3 gives the lookahead sweep of §6.3. Table S3: Separating mass achieved by exhaustive design at lookahead ℓ . depth d ℓ=1 =1 ℓ=2 =2 ℓ=3 =3 ℓ=4 =4 ℓ=5 =5 ℓ=6 =6 11 11 11 – – – – 22 00 11 11 – – – 33 00 00 11 11 – – 44 00 00 00 11 11 – 55 00 00 00 00 11 11 S7.3 End-to-end comparison at shallow depth Table S4 gives the corpus comparison of §6.4 in full. Table S4: One learner at a fixed budget on three corpora, as mean ± half-range over ten seeds. BF is the Bayes factor and L the log-likelihood. The zeros under π are exact rational zeros, so their spread is exactly zero by Theorem 6. Environment corpus log10 _10 BF coverage L/step∗ T-maze under π 0.00±0.000.00± 0.00 16.2±3.216.2± 3.2% −0.6932±0.0014-0.6932± 0.0014 random 300.91±9.03300.91± 9.03 99.9±0.399.9± 0.3% −0.4303±0.0449-0.4303± 0.0449 designed 300.91±9.03300.91± 9.03 99.9±0.399.9± 0.3% −0.4303±0.0449-0.4303± 0.0449 Rotating MAB under π 0.00±0.000.00± 0.00 8.4±1.78.4± 1.7% −0.6932±0.0008-0.6932± 0.0008 random 161.93±20.04161.93± 20.04 100.0±0.0100.0± 0.0% −0.6798±0.0082-0.6798± 0.0082 designed 148.86±17.89148.86± 17.89 29.5±3.329.5± 3.3% −0.6851±0.0070-0.6851± 0.0070 Cheat MAB under π 0.00±0.000.00± 0.00 29.5±3.329.5± 3.3% −0.6553±0.0173-0.6553± 0.0173 random 99.48±16.4699.48± 16.46 100.0±0.0100.0± 0.0% −0.6378±0.0222-0.6378± 0.0222 designed 99.48±16.4699.48± 16.46 100.0±0.0100.0± 0.0% −0.6378±0.0222-0.6378± 0.0222 Rotating Maze under π 0.00±0.000.00± 0.00 16.2±3.216.2± 3.2% −0.6741±0.0104-0.6741± 0.0104 random 87.41±13.1287.41± 13.12 100.0±0.0100.0± 0.0% −0.6301±0.0285-0.6301± 0.0285 designed 87.41±13.1287.41± 13.12 100.0±0.0100.0± 0.0% −0.6301±0.0285-0.6301± 0.0285 ∗ Held-out log-likelihood per step, taken over every held-out step and charging log(1/|O|) (1/|O|) for each step the model cannot score, so that all three rows of an environment are divided by the same denominator. The per-covered-step figure is not comparable across rows, since it conditions on whichever subset each model happens to cover and so flatters a corpus that covers only the easy steps. The random and designed rows are identical on three of the four environments because there the deviation assigns equal probability to every action. On the T-maze and Rotating Maze it mixes the two actions half and half, and on Cheat MAB it plays each of the three arms with probability 1/31/3. The two rows therefore describe the same policy and draw the same corpus under a shared seed. Rotating MAB is the one environment where they differ, and there the difference is smaller than either row’s spread over seeds, so the two corpora tie. The coverage column separates them. The designed corpus concentrates on the missing experiment and covers 29.529.5% of held-out steps against uniform exploration, which is the cost of design at a depth where design brings no gain. S7.4 Evidence against memorylessness This comparison places the true automaton against the memoryless null, a single-state model that serves as a null hypothesis. Large Bayes factors establish that the environments are non-Markovian and that the posterior detects it, which is a precondition for everything that follows. Table S5 reports the comparison at 40 trajectories of 8 steps, where every environment rejects memorylessness. Table S5: Log Bayes factor of the true automaton against a memoryless null. Environment States Non-Markovian structure log10 _10 BF T-maze 3 remember the initial cue 35.0635.06 Rotating MAB 2 reward probabilities rotate on every reward 8.038.03 Cheat MAB 3 an action sequence unlocks max reward 7.817.81 Rotating Maze 6 orientation rotates every 3 moves 9.849.84 (a) Evidence against memorylessness. (b) Posterior mass on the true structure. Figure S4: Rejection of memorylessness and structure recovery on the Tomita grammars. Figure S4 reports the same comparison on the seven Tomita grammars. Every grammar clears the threshold for decisive evidence by at least an order of magnitude, and the structure at the posterior mode is the true one in all seven cases. The Tomita languages are acceptors, so we encode each as an RDP with a single action a. The minimal DFA supplies the transition structure over O=0,1O=\0,1\, its acceptance labelling is discarded, and the state qiq_i of an n-state automaton, for i=0,…,n−1i=0,…,n-1, emits 00 with probability (i+1)/(n+1)(i+1)/(n+1), so no two states share an emission row. The corpus is 60 strings of 40 symbols, drawn by emitting o∼e(q,a)o e(q,a) and moving to δ(q,a,o)δ(q,a,o). For the five-state grammars (Tomita 3 and 7) we enumerate one canonical representative per state-renaming class, 160,675160,675 structures in place of 5105^10. With a single action there is no behaviour policy and no choice to decline, so this panel tests the structure-level machinery alone and carries no policy-relative content. S7.5 Recovery of emission probabilities Table S6: Posterior-mean emission probabilities against the truth. Environment Rows visited Mean abs. err Max abs. err Min samples/row T-maze 6/6 0.0310.031 0.0600.060 17 Rotating MAB 6/6 0.0300.030 0.0670.067 41 Cheat MAB 9/9 0.0510.051 0.1670.167 20 Rotating Maze 12/12 0.0770.077 0.3650.365 7 The maximum error tracks the sparsest row, which indicates sampling error. On Rotating Maze the mean absolute error falls from 0.07690.0769 to 0.02810.0281, 0.01510.0151, and 0.00950.0095, and the maximum error falls from 0.3650.365 to 0.1200.120, 0.0480.048, and 0.0220.022, as the number of trajectories goes from 4040 to 160160, 640640, and 25602560, so the maximum error falls by a factor of about 1717. (a) Evidence against trajectory count. (b) Emission error against trajectory count. Figure S5: Scaling of evidence and emission error, averaged over five seeds. Figure S5 shows both rates on logarithmic axes. Evidence for history-dependence runs parallel to a slope-one reference, so the log Bayes factor grows close to linearly in the number of trajectories, rising on the T-maze from 2.702.70 to 163.47163.47 between 5 and 160 trajectories. Emission error follows the n−1/2n^-1/2 reference, which rules out a systematic failure on the sparsest row. Remark 20 (A caveat on identifiability). Structure recovery presupposes that the automaton states differ in behaviour. Two states carrying the same emission distribution are merged under any amount of data. S7.6 Ablations Tables S5 and S6 report a single seed. Table S7 gives their variation over 12 seeds, and the minimum over seeds remains decisive in every environment. Figure S3 plots the quantities of this subsection. Table S7: Variation of the main quantities over 12 seeds. BF: Bayes factor; MAE: mean absolute error; sd: standard deviation. Environment log10 _10 BF mean ± sd min log10 _10 BF over seeds emission MAE mean ± sd T-maze 37.36±2.0737.36± 2.07 34.8234.82 0.044±0.0150.044± 0.015 Rotating MAB 10.78±3.0910.78± 3.09 6.276.27 0.045±0.0180.045± 0.018 Cheat MAB 11.12±3.2911.12± 3.29 6.376.37 0.051±0.0160.051± 0.016 Rotating Maze 10.41±1.9910.41± 1.99 8.478.47 0.065±0.0140.065± 0.014 Prior strength. Sweeping the Dirichlet concentration over α∈1,2,3,5,10α∈\1,2,3,5,10\, the log Bayes factor declines steadily and never changes sign. It falls from 35.135.1 to 24.424.4 on the T-maze, from 8.08.0 to 6.86.8 on Rotating MAB, from 7.87.8 to 5.35.3 on Cheat MAB, and from 9.89.8 to 6.26.2 on Rotating Maze. Small-data crossover. At 2 trajectories, 7 of the 12 seeds on the T-maze favour the memoryless null, which is the correct preference for a simpler model, since two trajectories do not justify three states. The T-maze is the only environment in which a strict majority of seeds does so, with 6 of 12 on Cheat MAB. By 10 trajectories 1 of the 48 seeds still favours the null, and every mean is positive. Deviation strength. Section S7.8 reports this sweep, where the non-monotone behaviour of Cheat MAB is the informative case. S7.7 Comparison with the reachability criterion On the T-maze, reachability assigns every candidate deviation the same score. The cue is drawn on the first step whatever the agent does, so the behaviour policy already visits every automaton state, and the reachability score stays constant across all candidate deviations, which leaves the criterion with no preference among them. This blindness does not extend to every non-Markovian problem, and the four environments of the suite split into two groups (Table S8). Table S8: Form of the separating evidence in each environment. Environment Separating evidence is… Reachability T-maze, Rotating MAB an action taken in an already-visited state blind (score constant) Cheat MAB, Rotating Maze a state the policy never reaches informative When the missing experiment is to reach a state q, reachability is the right criterion, which is the case LMDP∗L^*_MDP addresses. It gives no signal only when the policy already visits every automaton state and the distinguishing evidence is which action was taken there. Reachability is therefore complete for the state-reachability subclass and uninformative outside it, and the T-maze shows that the complement of that subclass is nonempty. Expected information gain distinguishes the deviations from the behaviour policy on all four environments, taking the value zero under the behaviour policy and a positive value under every deviation. S7.8 Dependence on deviation strength Definition of p. The deviation strength p is the probability the deviating policy assigns to the one action the behaviour policy declines, with the remaining mass spread uniformly over the other actions. Table S9: The deviation πp′π _p in each environment. At p=0p=0 the deviation is the behaviour policy, and p is the probability of the named action at every step. Environment Behaviour policy π Action taken w.p. p Remaining mass T-maze always waitwait runrun waitwait, w.p. 1−p1-p Rotating MAB always arm0arm0 arm1arm1 arm0arm0, w.p. 1−p1-p Cheat MAB never arm2arm2 arm2arm2 arm0,arm1arm0,arm1, w.p. (1−p)/2(1-p)/2 each Rotating Maze always staystay movemove staystay, w.p. 1−p1-p The value used everywhere else in the paper is p=1/2p=1/2, except on Cheat MAB where it is p=1/3p=1/3, so that the three arms are exercised comparably. The sweep below varies p over its whole range on Cheat MAB, which is the environment where the dependence is not monotone. The choice of deviation matters for a second reason, independent of the comparison with LMDP∗L^*_MDP. Sweeping the deviation probability p from 00 to 11 on Cheat MAB gives the following: Table S10: Separating mass on Cheat MAB against deviation strength p. p 00 1/81/8 1/41/4 3/83/8 1/21/2 5/85/8 3/43/4 7/87/8 11 separating mass 0 7/1287/128 3/323/32 15/12815/128 /1/8 15/12815/128 3/323/32 7/1287/128 0 (a) Separating mass. (b) Expected information gain. Figure S6: Deviation strength swept from the behaviour policy to its opposite. Figure S6 shows the separating mass and the expected information gain over the same sweep in all four environments. The cheat sequence is (arm1,arm2)(arm1,arm2). A policy that always plays arm2arm2 therefore never plays arm1arm1, never completes the sequence, and never unlocks the payoff. A heuristic that explores more arrives at p=1p=1 and learns nothing, because only the correct history pattern separates the models. On the other three environments the sweep is monotone, which makes Cheat MAB the informative case. S7.9 Pec under estimated emission tables The identifiability results of this paper are computed from exact rational emission tables, and Definition 11 accordingly tests emission rows for exact inequality. In practice the tables are estimated from counts, and two rows estimated from the same distribution differ with probability approaching one as the corpus grows. The exact test then reports a disagreeing pair with probability approaching one, so Pec almost never certifies π-equivalence on estimated tables. The certificate is the main output of the procedure, so this is the respect in which the results here depend on exactness. The tolerant test. Section 5.4 replaces the test in Definition 11 by maxo|e(q,a)(o)−e′(q′,a)(o)|>τ _o|e(q,a)(o)-e (q ,a)(o)|>τ. With η the sup-norm error of the estimated tables over the rows Pec consults and γ the smallest sup-norm separation among pairs whose exact rows disagree, the tolerant test returns the exact-arithmetic verdict on every pair whenever 2η<τ<γ−2η,2η\;<\;τ\;<\;γ-2η, a window that is non-empty as soon as η<γ/4η<γ/4 and that opens at a finite sample size. Table S11: Pec on estimated emission tables, corridor family, 600 trajectories per candidate under a covering policy, five seeds. η is measured over the rows the procedure consults. depth d γ η window τ=0τ=0 τ in window 22 1/21/2 0.0720.072 (0.144, 0.356)(0.144,\,0.356) never certifies all correct 44 1/21/2 0.0830.083 (0.167, 0.333)(0.167,\,0.333) never certifies all correct 66 1/21/2 0.0980.098 (0.195, 0.305)(0.195,\,0.305) never certifies all correct 88 1/21/2 0.0950.095 (0.190, 0.310)(0.190,\,0.310) never certifies all correct In Table S11, at τ=0τ=0 the estimated rows never agree, so the exact test is unusable on estimates. At every τ strictly inside the window, sampled at eight points per row, the tolerant test reproduces exact arithmetic, certifying π-equivalence under the behaviour policy and still returning the witness under the deviation. At τ=γ+2ητ=γ+2η, above the window, it certifies the deviation as well, which is a false certificate, so the upper bound of the window cannot be dropped. Choice of estimation policy. Estimating the tables under a uniform policy makes η grow with depth, reaching 0.190.19 at d=8d=8 and closing the window. The cause is the structure of the corridor. Reaching room d−1d-1 requires d−1d-1 waits in succession, so under uniform exploration the deep rooms are visited a 2−(d−1)2^-(d-1) fraction of the time and their rows are estimated worst, and they are exactly the rows that carry the missing experiment. Weighting the estimation policy towards traversal restores the window at every depth. The same observation motivates designing the experiment, and here it applies to the estimation of the tables. Near-equivalent candidates. The window closes as γ approaches zero. For any fixed γ>0γ>0 it still opens at a finite sample size, although that size grows without bound as the candidates approach equivalence. The posterior likewise still moves, more slowly as the separation decreases. This gradual degradation is the quantitative counterpart of Theorem 6. A continuous observation space enters this account the same way, through state aliasing that shrinks γ (Appendix S8). S7.10 Equivalence testing as an exploration strategy Section 6.4 compares designed experiments against uniform exploration. Modern active automata learning explores better than uniformly, and Table S12 measures by how much. AALpy (Muskardin et al., 2022) ships two standard strategies for answering equivalence queries, and both decompose into ingredients evaluated elsewhere in this paper. The random-walk strategy explores by uniform random actions with a reset probability, which is the random corpus of §6.4. The state-prefix strategy replays an access sequence to a hypothesis state and then continues at random, and its first ingredient is the state-reachability criterion of §S7.7. We score all three strategies by the exact probability of producing a history on which the candidates disagree. Table S12: Separating mass of each exploration strategy on the corridor family, as exact rationals. depth d random walk state prefix designed prefix / walk 22 1/41/4 3/83/8 11 1.5×1.5× 44 1/161/16 15/6415/64 11 3.8×3.8× 66 1/641/64 21/12821/128 11 10.5×10.5× 88 1/2561/256 255/2048255/2048 11 31.9×31.9× On this family the access-sequence prefix improves on the random walk, because the missing experiment sits behind a state the walk has to reach. The prefix converts an exponential decay into a polynomial one, and the state-prefix strategy beats the random walk by a factor that grows to 3232 at depth eight. The polynomial is 1/d1/d, since the product of depth and separating mass is 0.7500.750, 0.9380.938, 0.9840.984 and 0.9960.996 down the column. The rate follows from the strategy, which cycles through d hypothesis states and so spends a 1/d1/d fraction of its budget on the room that carries the experiment, probing there with probability 1/21/2 at the first opportunity and with the remaining mass later. A designed deviation executes the separating sequence every time and has separating mass 11 at every depth, so the state-prefix strategy still falls short of the experiment. Table S12 therefore places the gap between designed experiments and a competent active-learning heuristic below the gap against uniform exploration reported in Table 3, without closing it. Table S13: The same strategies on the T-maze, where every automaton state is visited on the first step whatever the agent does. random walk state prefix designed separating mass 1/21/2 1/21/2 11 Table S13 isolates the prefix ingredient. On the T-maze the cue is drawn on the first step whatever the agent does, so every automaton state is already visited, no access sequence changes what the strategy sees, and the state-prefix strategy collapses exactly onto its random-walk tail, with the two entries equal as rationals. This is the blindness of the reachability criterion recorded in §S7.7, here measured on a named implementation. On this subclass the reachability ingredient contributes nothing, and whatever the strategy achieves it achieves by walking at random. Scope of the comparison. These are exploration strategies scored on a fixed pair of candidates, and the comparison does not replicate LMDP∗L^*_MDP or AALpy’s learning loop. Both strategies exist to answer conjectures against a live system inside an active learning algorithm, and neither is available in the offline setting this paper addresses, where the corpus cannot be extended. The measurement is meaningful because the ingredient that does the work in an equivalence test, the choice of where to go before acting at random, is the quantity our design step chooses, so the two can be compared without running either algorithm outside its assumptions. S7.11 Computation of RegORL’s distinguishability parameter Section S5.2 argues that Pec and RegORL (Cipollone et al., 2023) produce objects that are not commensurable as estimators, although the parameter on which the RegORL guarantee rests can be computed exactly on our environments. The parameter. RegORL’s guarantee rests on its Assumption 2, that the behaviour policy has L∞pL^p_∞-distinguishability at least μ0>0 _0>0. For a minimal RDP with layered states Q=⋃tQtQ= _tQ_t, μ0 _0 is the largest value such that, for every t and every pair of distinct q,q′∈Qtq,q ∈ Q_t, the L∞pL^p_∞ distance between the distributions of the trace from step t onwards, started in q and in q′q under π, is at least μ0 _0. That distance is the largest difference, over trace prefixes within the remaining horizon, between the probabilities that the two traces begin with the prefix. In the notation of Cipollone et al. (2023), where Q, A, O and R denote the numbers of states, actions, observations and rewards, H the horizon, δ the failure probability and dminbd^b_ their concentrability term, their Theorem 6 requires a corpus of size Nδ= 21log(8QAO/δ)Hlog(2ARO)/(dminbμ0),N_δ\;=\;21 (8QAO/δ) H (2ARO)\,/\,(d^b_ _0), so μ0 _0 enters in the denominator at the first power and the requirement diverges as it goes to zero. Two features of the definition matter below. The probability of a trace prefix includes the policy’s own action probabilities, so an action π never takes contributes zero to both sides and separates nothing. The quantifier also ranges over states of the minimal RDP, minimal in the Moore sense, so two states of a layer that no input sequence separates within the steps the episode has left count as one state. That quotient is taken with respect to the dynamics, independently of π, and it cannot be skipped, since without it every fixed-horizon RDP would report μ0=0 _0=0 from its last layer, where nothing has time to separate, and the parameter would say nothing about any policy. Evaluation on the four environments. Table 1 reports μ0 _0 on the four environments. On three of them μ0=0 _0=0 as an exact rational, so Assumption 2 fails, NδN_δ diverges, and the RegORL guarantee is vacuous, and on each of them the separating mass is also an exact rational zero. Two of those three are benchmarks from Abadi and Brafman (2020). The state pair that attains the minimum is qLq_L against qRq_R at t=2t=2 on the T-maze, and the two automaton states at t=2t=2 on each MAB. On Rotating Maze the assumption instead holds trivially. The behaviour policy never moves, so it reaches a single state per layer, no pair of distinct states exists to be told apart, and the minimum is over the empty set. The same is true of every member of the corridor family of §6.3, where waiting advances the corridor deterministically. Their parameter therefore does not vanish on every instance ours flags. Their μ0 _0 compares two states of the true model that the policy reaches, whereas π-equivalence compares two candidate models, so an ambiguity confined to a region the policy never enters leaves Assumption 2 satisfied while Pec certifies π-equivalence. On those instances the RegORL bound binds through its concentrability condition instead. Conversely, μ0 _0 vanishes whenever the policy cannot separate two states of the true model, even when the candidate under test differs from the truth on an action the policy takes, in which case Pec reports the pair as distinguishable. The two criteria therefore overlap without either containing the other. Deciding Assumption 2 with Pec. Section 6.1 shows that μ0>0 _0>0 is decided by running Pec from each same-layer pair and comparing the separating horizon it reports against the number of steps the episode has left. We checked this against the exact parameter on every pair of every environment and of the corridor family, and the two agree everywhere. Table S14 reports the cost on the corridor family, where the ratio between the cost of the definition and that of Pec grows from 3.7×3.7× at depth 2 to 67.5×67.5× at depth 7. Table S14: The corridor family: μ0 _0 under the deviation, and the cost of deciding Assumption 2 from the definition versus with Pec. Under π the assumption holds trivially at every depth while Pec certifies π-equivalence at every depth. depth d μ0 _0 under π′π ratio to d−1d-1 definition (s) Pec (s) speedup 22 1/41/4 – 0.00050.0005 0.000140.00014 3.7×3.7× 33 1/161/16 0.2500.250 0.00240.0024 0.000540.00054 4.4×4.4× 44 1/641/64 0.2500.250 0.01000.0100 0.001430.00143 7.0×7.0× 55 1/2561/256 0.2500.250 0.04080.0408 0.003140.00314 13.0×13.0× 66 1/10241/1024 0.2500.250 0.16160.1616 0.005670.00567 28.5×28.5× 77 1/40961/4096 0.2500.250 0.65360.6536 0.009690.00969 67.5×67.5× Decay of μ0 _0 with depth. On the corridor family, μ0 _0 under the deviation falls by a factor of exactly 44 per room. Since Nδ∝1/μ0N_δ 1/ _0, the corpus RegORL needs grows like 4d4^d in the separating horizon even after the assumption holds. This is the decay that motivated the formal-language metric of Deb et al. (2025), which §1 cites, and we exhibit it here as exact rationals on a family where depth is the only thing varying. It is also the exponential in the separating horizon that §6.4 measures from the data side. S7.12 Pec at scale Corollary 13 states a running time linear in |Q|⋅|Q′|⋅|A|⋅|O||Q|·|Q |·|A|·|O| and independent of the horizon. Our environments are small because the method requires a known pair (§6), so we measure the bound on constructed pairs instead, sweeping the product automaton from 10210^2 to 10610^6 state pairs. Worst-case instances. The bound describes the certifying run. When Pec returns a witness it stops at the first disagreeing pair and touches only the part of the product that precedes it, whereas when it certifies π-equivalence it must exhaust the reachable product. The sweep is therefore built from π-equivalent pairs, and the shape of those pairs is forced. If every pair in Q×Q′Q× Q is reachable and none disagrees, then e(q,a)=e′(q′,a)e(q,a)=e (q ,a) for all q,q′q,q and every a∈Aπa∈ A_π, so both emission tables are constant on the actions the policy takes, since any variation would create a disagreeing pair and hence an early return. A full product with no early exit thus forces flat emissions under AπA_π, with the models differing on an action outside it. The corridor construction of §6.3 has the same form, and instances of this form are the worst case for the procedure. The instances are two cycles of coprime lengths n and m advanced by the policy’s action. From (0,0)(0,0) the product walks (tmodn,tmodm)(t n,\,t m), which by the Chinese remainder theorem visits all nmn\,m pairs, so the reachable product is exactly |Q|⋅|Q′||Q|·|Q |. Table S15: Pec certifying π-equivalence. Every pair of the product is reachable, so the procedure explores all of it before answering. |Q||Q| |Q′||Q | product pairs explored seconds µs / pair 1010 1111 110110 110110 0.00050.0005 4.504.50 5050 5151 2,5502,550 2,5502,550 0.01110.0111 4.364.36 100100 101101 10,10010,100 10,10010,100 0.04380.0438 4.344.34 200200 201201 40,20040,200 40,20040,200 0.17770.1777 4.424.42 500500 501501 250,500250,500 250,500250,500 1.12631.1263 4.504.50 700700 701701 490,700490,700 490,700490,700 2.22822.2282 4.544.54 10001000 10011001 1,001,0001,001,000 1,001,0001,001,000 4.64574.6457 4.644.64 The cost per pair is flat to within 8%8\% across four orders of magnitude, and the least-squares slope of log(time) (time) against log(pairs) (pairs) over the seven sizes tabulated is 1.0031.003, consistent with the linear growth in |Q|⋅|Q′||Q|·|Q | that the bound asserts at fixed |A||A| and |O||O|. Holding the product fixed at 40,20040,200 and enlarging the action support instead gives 0.1790.179, 0.3300.330, 0.4870.487 and 0.6040.604 seconds for |Aπ|=1,2,3,4|A_π|=1,2,3,4, which isolates the |A||A| factor. Random transition tables. Replacing the cycles with random transition tables gives a reachable product between 38.7%38.7\% and 49.5%49.5\% of |Q|⋅|Q′||Q|·|Q |, with a comparable 4.54.5–5.25.2 µs per pair and a log-log slope of 1.0251.025 against the pairs explored. At |Q|=1000|Q|=1000 that is 419,192419,192 pairs in 2.172.17 seconds. The linear scaling therefore comes from the procedure and does not depend on the cycle construction. Cost of finding a witness. Fixing the product at 1,001,0001,001,000 and moving only the depth at which the two models disagree, Pec returns in 1.8×10−51.8× 10^-5, 8.1×10−58.1× 10^-5, 7.4×10−47.4× 10^-4 and 7.2×10−37.2× 10^-3 seconds at depths 00, 1010, 100100 and 999999, against 4.654.65 seconds to certify the same product. Even at depth 999999 the search touches a thousandth of the pairs a certificate needs. An instance whose corpus is insufficient therefore pays the full bound, while candidates that separate early cost almost nothing. Independence from the horizon. None of these runs takes a horizon as input, and answers the infinite-horizon question. Enumerating histories answers only a finite-horizon question, at a cost exponential in the horizon. Appendix S8 Limitations and Open Problems Almost-sure convergence is not formalised, since §S6.2 supplies every hypothesis Doob’s theorem requires but the statement itself needs the trajectory measure. The design procedure of §6.2 is open-loop, and whether the lookahead bound of Table S3 is tight for a closed-loop designer remains open. Scaling beyond the five automaton states that exact enumeration handles requires approximate inference, which this paper does not study. Designed experiments give no gain at short separating horizons (§6.4), the reachability comparison holds only for the subclass identified in §S7.7, an access-sequence heuristic narrows the gap in separating mass between designed experiments and uniform exploration from a factor of 256256 to a factor of about 88 at depth eight (§S7.10), and the freezing mechanism itself is known in off-policy evaluation and causal inference. Continuous observations would enter the account through aliasing that shrinks the separation γ of Appendix S7.9, and the window of the tolerant test would close as γ shrinks.