Categorizer Automata for Discounted-Sum Payoffs

We study formal policy synthesis for continuous-state stochastic systems under linear temporal logic specifications. The product of the system with the automaton of the specification has a hybrid state space with sparse rewards. We introduce a generalized optimal backup order, defined in reverse to a topological order over automaton states, that guides value backups and provably preserves optimality. We further present a model-free actor-critic algorithm whose policy evaluation solves a constrained optimization problem by the augmented Lagrangian method, yielding hyperparameter self-tuning, and prove its optimality and convergence in the tabular case. Since integer encodings of automaton states impose a spurious ordinal relationship on functions learned by one network, we dedicate a value and a policy network to each automaton state (modular learning). The algorithm matches or outperforms PPO, DQN, and A2C on CartPole, and on a Dubins car under a temporal specification the topological order and modular learning raise the success rate from 26.0% to 71.5%.

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.

We study finite-iteration behavior of asynchronous categorical distributional temporal-difference methods, covering scalar categorical TD (CTD) in the Cramér geometry and multivariate signed-categorical TD (MTD) in the maximum mean discrepancy (MMD) geometry. We establish high-probability guarantees under i.i.d. sampling and under a continuing Markovian trajectory. For CTD, the Cramér sample complexity to the true return law has leading term $\tilde O(ρ_{\min}^{-1}(1-γ)^{-2}\varepsilon^{-2})$ in the i.i.d. and $\tilde O(μ_{\min}^{-1}(1-γ)^{-2}\varepsilon^{-2}+μ_{\min}^{-1}t_{\mathrm{mix}})$ in the Markovian setting, without using variance reduction or data dropping. For MTD, the MMD sample complexity has leading terms $\tilde O(ρ_{\min}^{-1}(1-γ)^{-1-c}\varepsilon^{-2})$ and $\tilde O(μ_{\min}^{-1}(1-γ)^{-1-c}\varepsilon^{-2}+μ_{\min}^{-1}t_{\mathrm{mix}})$, where $c\in(0,2)$ is the homogeneity exponent of the MMD kernel, and they reduce to the CTD rates when $c=1$. These are, to our knowledge, the first finite-iteration rates for MTD. For undiscounted fixed-horizon policy evaluation, the same analysis applies to fixed-horizon versions of CTD and MTD under i.i.d. and episodic sampling, and the rates match the discounted ones with the effective horizon $(1-γ)^{-1}$ replaced by the horizon $H$ in the leading term. Matching minimax lower bounds show that the leading terms, and the implied $1$-Wasserstein rates, are optimal under i.i.d., Markovian, and episodic sampling. Together, these results provide a unified non-asymptotic analysis of asynchronous categorical distributional TD across scalar, multivariate, discounted, and fixed-horizon settings, with rates that are minimax optimal in their leading terms.