Probabilistic Alternating Simulations for Policy Synthesis in Uncertain Stochastic Dynamical Systems

TL;DR

This paper introduces probabilistic alternating simulation relations to enable formal policy synthesis in uncertain stochastic systems with both stochastic and nondeterministic disturbances, extending existing methods.

Contribution

It extends probabilistic simulation relations to systems with combined stochastic and nondeterministic disturbances, inspired by alternating simulation, for more robust policy synthesis.

Findings

Successfully applied to a 4D-state Dubins vehicle.

Enables reasoning over both probabilistic and adversarial uncertainties.

Generalizes existing simulation relations for verification and control synthesis.

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.