Data-Driven Abstraction and Synthesis for Stochastic Systems with Unknown Dynamics

TL;DR

This paper introduces a data-driven method for creating finite-state abstractions of stochastic systems with unknown nonlinear dynamics, enabling the synthesis of control policies that satisfy probabilistic specifications with confidence.

Contribution

It presents a novel technique to construct finite-state interval MDP abstractions using only noisy observations and Lipschitz bounds, facilitating correct-by-construction control policy synthesis.

Findings

Effective abstraction from noisy data.

Robust policy synthesis with probabilistic guarantees.

Successful experimental validation.

Abstract

We study the automated abstraction-based synthesis of correct-by-construction control policies for stochastic dynamical systems with unknown dynamics. Our approach is to learn an abstraction from sampled data, which is represented in the form of a finite Markov decision process (MDP). In this paper, we present a data-driven technique for constructing finite-state interval MDP (IMDP) abstractions of stochastic systems with unknown nonlinear dynamics. As a distinguishing and novel feature, our technique only requires (1) noisy state-input-state observations and (2) an upper bound on the system's Lipschitz constant. Combined with standard model-checking techniques, our IMDP abstractions enable the synthesis of policies that satisfy probabilistic temporal properties (such as "reach-while-avoid") with a predefined confidence. Our experimental results show the effectiveness and robustness of our approach.