arXiv · 2508.05062
Probabilistic Alternating Simulations for Policy Synthesis in Uncertain Stochastic Dynamical Systems
Abstract
A classical approach to formal policy synthesis in stochastic dynamical systems is to construct a finite-state abstraction, often represented as a Markov decision process (MDP). The correctness of these approaches hinges on a behavioural relation between the dynamical system and its abstraction, such as a probabilistic simulation relation. However, probabilistic simulation relations do not suffice when the system dynamics are, next to being stochastic, also subject to nondeterministic (i.e., set-valued) disturbances. In this work, we extend probabilistic simulation relations to systems with both stochastic and nondeterministic disturbances. Our relation, which is inspired by a notion of alternating simulation, generalises existing relations used for verification and policy synthesis used in several works. Intuitively, our relation allows reasoning probabilistically over stochastic uncertainty, while reasoning robustly (i.e., adversarially) over nondeterministic disturbances. We experimentally demonstrate the applicability of our relations for policy synthesis in a 4D-state Dubins vehicle.
Explore related subjects
Keep this discovery
Thom Badings, Alessandro Abate. 2025-08-07. Probabilistic Alternating Simulations for Policy Synthesis in Uncertain Stochastic Dynamical Systems. https://arxiv.org/abs/2508.05062
Cite the original work for its findings. Save a collection to share your selection of sources.