Data-Driven Strategy Synthesis for Stochastic Systems with Unknown Nonlinear Disturbances

TL;DR

This paper presents a data-driven method for synthesizing provably-correct controllers for nonlinear switched systems with unknown disturbances, ensuring high probability of satisfying complex temporal logic specifications.

Contribution

The paper introduces a novel framework combining disturbance learning, robust MDP construction, and automata-based synthesis for nonlinear systems with unknown disturbances.

Findings

High satisfaction probabilities in empirical tests

Effective disturbance ambiguity set learning

Provable correctness guarantees

Abstract

In this paper, we introduce a data-driven framework for synthesis of provably-correct controllers for general nonlinear switched systems under complex specifications. The focus is on systems with unknown disturbances whose effects on the dynamics of the system is nonlinear. The specifications are assumed to be given as linear temporal logic over finite traces (LTLf) formulas. Starting from observations of either the disturbance or the state of the system, we first learn an ambiguity set that contains the unknown distribution of the disturbances with a user-defined confidence. Next, we construct a robust Markov decision process (RMDP) as a finite abstraction of the system. By composing the RMDP with the automaton obtained from the LTLf formula and performing optimal robust value iteration on the composed RMDP, we synthesize a strategy that yields a high probability that the uncertain system satisfies the specifications. Our empirical evaluations on systems with a wide variety of disturbances show that the strategies synthesized with our approach lead to high satisfaction probabilities and validate the theoretical guarantees.