Confidence Sequences for Online Statistical Model Checking of Markov Decision Processes

Learning-based approaches to verifying unknown Markov decision processes (MDPs) often employ uncertain MDPs. These models use, for example, confidence intervals to capture transition uncertainty and allow synthesis of policies that are robust to this uncertainty. However, this approach typically quantifies uncertainty independently for individual transition probabilities, ignoring dependencies due to shared latent quantities. We propose to learn such models using parametric MDPs (pMDPs), where transition probabilities are expressions over a set of parameters. We project statistical uncertainty from empirical transition frequencies onto the pMDP's parameter space, yielding a probably approximately correct (PAC) uncertainty model for the underlying MDP that respects the algebraic dependencies between transitions. The resulting models are algorithmically challenging to solve, so we propose a hierarchy of sound polytopic outer approximations of the induced confidence set. We implement and evaluate our approach, demonstrating substantially tighter uncertainty estimates than classical interval-based uncertain MDP learning techniques.

Probabilistic model checking for Markov decision processes (MDPs) provides quantitative guarantees, but often offers limited insight into why undesired outcomes occur. Probability-raising (PR) causality addresses this by identifying states whose visitation increases the probability of reaching designated states. Existing PR-cause identification methods, however, use MDP modifications not well-suited for learning: the gap between conditional and unconditional reachability probabilities can be hard to detect from transition samples, and construction requires reachability probabilities of the MDP, which are unavailable when transition probabilities are unknown. We study unknown MDPs and propose a learning approach with probabilistic guarantees for PR-cause identification. Our key ingredient is a restart-based MDP modification that reduces PR-cause checking to two conditional reachability queries without using reachability values of the original MDP. We prove correctness, establish sample-complexity bounds, and develop an anytime learning-and-checking algorithm based on two-sided value iteration that progressively classifies states as causal, non-causal, or undecided. Experiments on two benchmarks demonstrate reliable and fast identification of PR causes.

Learning the optimal policy for Markov decision process problems (MDPs) from samples is a fundamental problem in online and data-driven decision-making. Function approximations are usually deployed to handle large or infinite state-action space. In our work, we consider the MDP problems with function approximation and we develop a new algorithm to solve it efficiently. Our algorithm is based on a linear programming (LP) reformulation and repeatedly resolves the identified reduced linear system as new transition samples arrive. After the optimal basis is identified, we show that, after $N$ resolving rounds, the expected averaged iterate achieves an instance-dependent $\widetilde O(C_{\mathrm{inst}}/N)$ objective shortfall and signed constraint residual. We separately account for the historical samples used for basis identification and the $d_2$ transition queries used in each resolving round, which yields the corresponding total transition-query complexity. We further complement our result with a \textit{robust} $O(1/\sqrt{N})$ bound that is independent of $Δ$. In comparison to the guarantees established in the previous literature, our instance dependent guarantee is tighter when the underlying instance is favorable, and the numerical experiments also reveal the wide applications and efficient empirical performances of our algorithms.