Organizations: Nanyang Technological University, Singapore · Tata Institute of Fundamental Research, Mumbai, India · Université Libre de Bruxelles, Brussels, Belgium · IITB Trust Lab, Department of CSE, IIT Bombay, Mumbai, India
Abstract
Partially Observable Markov Decision Processes (POMDPs) are the standard framework for decision-making under uncertainty. While sampling-based methods scale well, they lack formal correctness guarantees, making them unsuitable for safety-critical applications. Conversely, formal synthesis techniques provide correctness-by-construction but often struggle with scalability, as general POMDP synthesis is undecidable. To bridge this gap, we propose a synthesis framework that integrates sampling, automata learning, and model-checking. Inspired by Angluin's L∗ algorithm, our approach utilizes sampling as a membership oracle and model-checking as an equivalence oracle. This enables the synthesis of finite-state controllers with formal guarantees, provided the sampling-induced policy is regular. We establish a relative completeness result for this framework. Experimental results from our prototypical implementation demonstrate that this method successfully solves threshold-safety problems that remain challenging for existing formal synthesis tools. We believe our algorithm serves as a valuable component in a portfolio approach to tackling the inherent difficulty of POMDP synthesis problems.
Synthesising autonomous agents that can navigate uncertain environments while adhering to complex temporal constraints remains a fundamental challenge. While Linear Temporal Logic (LTL) provides a rigorous language for specifying such tasks, the inherent undecidability of qualitatively verifying LTL satisfaction in partially observable Markov decision processes renders quantitative synthesis difficult, especially when designing reliable reward signals for approximate solvers. In this paper, we bridge this gap with a novel, sound reward-shaping mechanism that dynamically generates belief-dependent rewards grounded in certified LTL satisfaction. By integrating this mechanism into an enhanced Monte Carlo Planning framework, we empower agents to navigate the `fog' of partial observability with a search process focused on maximising verifiable success. Our experiments demonstrate that this approach not only thrives in scenarios where existing solvers fail but also maintains effectiveness and scalability across diverse benchmark domains.
We present an optimization-based framework for robust permissive synthesis for Interval Markov Decision Processes (IMDPs). While robust IMDP controller synthesis typically yields a single policy and most permissive-synthesis methods assume exact transition models, we synthesize multi-strategies that retain multiple actions while guaranteeing satisfaction of probabilistic reachability or expected-reward specifications under all admissible transition probabilities. We formulate the problem as a mixed-integer linear program (MILP) that maximizes the number of enabled state--action pairs subject to robust Bellman constraints. We develop two encodings: a direct vertex-enumeration formulation and a dualization-based formulation that avoids explicit enumeration of uncertainty-polytope vertices and has size linear in the number of successor transitions. Experiments on four benchmark domains show that both encodings achieve the same optimal permissiveness and scale to IMDPs with hundreds of thousands of states. Compared with standard robust single-policy synthesis, the resulting multi-strategies retain substantially more action choices.
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.