Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Ibon Gracia, Dimitris Boskos, Luca Laurenti, Morteza Lahijanian

TL;DR

This work addresses formal controller synthesis for discrete-time switched stochastic systems with unknown disturbance laws under $LTL_f$ specifications. It introduces a data-driven pipeline that builds a Wasserstein ambiguity set around the empirical disturbance distribution, constructs a finite IMDP abstraction, and extends it to a distributionally robust MDP to capture all distributions within the ambiguity set. By forming the product with a DFA for the $LTL_f$ formula and applying robust dynamic programming, the method yields a strategy that maximizes the worst-case probability of satisfying the specification, with correctness guarantees that hold with probability at least $1-\beta$. Empirical benchmarks across multiple nonlinear disturbances show high satisfaction probabilities and demonstrate that the approach tightens bounds with more data while clustering mitigates computational burden. Key contributions include a sound data-driven abstraction for nonlinear disturbances, a distributionally robust synthesis procedure under $LTL_f$, and extensive validation with theoretical guarantees and practical scalability.

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.

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

TL;DR

This work addresses formal controller synthesis for discrete-time switched stochastic systems with unknown disturbance laws under specifications. It introduces a data-driven pipeline that builds a Wasserstein ambiguity set around the empirical disturbance distribution, constructs a finite IMDP abstraction, and extends it to a distributionally robust MDP to capture all distributions within the ambiguity set. By forming the product with a DFA for the formula and applying robust dynamic programming, the method yields a strategy that maximizes the worst-case probability of satisfying the specification, with correctness guarantees that hold with probability at least . Empirical benchmarks across multiple nonlinear disturbances show high satisfaction probabilities and demonstrate that the approach tightens bounds with more data while clustering mitigates computational burden. Key contributions include a sound data-driven abstraction for nonlinear disturbances, a distributionally robust synthesis procedure under , and extensive validation with theoretical guarantees and practical scalability.

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.
Paper Structure (15 sections, 4 theorems, 15 equations, 4 figures, 1 table)

This paper contains 15 sections, 4 theorems, 15 equations, 4 figures, 1 table.

Table of Contents

  1. Introduction
  2. Problem Formulation
  3. Overview of the approach
  4. Preliminaries on Robust Markov Decision Processes
  5. Robust MDP Abstraction
  6. Learning the Unknown Probability Distribution
  7. States, Actions and Labeling Function of the Abstraction
  8. Transition Probability Distributions of the Abstraction
  9. Accounting for the discretization error
  10. Accounting for the Distributional Ambiguity
  11. Strategy Synthesis
  12. Correctness
  13. Case Studies
  14. Conclusion and Future Work
  15. Acknowledgements

Key Result

Lemma 4.1

Given $s\in \mathbb N$, $l\in[1,\infty]$, and $N$ i.i.d. samples $\textbf{w}^{(1)},\ldots,\textbf{w}^{(N)}$ from $P_{w}$, define their empirical distribution as $\widehat{P}_w := \frac{1}{N}\sum_{i=1}^N\delta_{\textbf{w}^{(i)}}$. Further, let $\phi$ be the diameter of $W$ in the $\infty$-norm, $\be where contains $P_w$ with confidence $1-\beta$.

Figures (4)

  • Figure 1: $N = 10^4$
  • Figure 2: $N = 8\times10^4$
  • Figure 3: $N = 10^5$
  • Figure 4: $N = 10^6$

Theorems & Definitions (14)

  • Definition 3.1: Robust MDP
  • Lemma 4.1: Ambiguity set
  • proof
  • Proposition 4.2
  • proof
  • Definition 4.3: Transition Probability Distributions of the RMDP Abstraction
  • Proposition 4.4: Soundness of the abstraction
  • proof
  • Remark 4.5: Clustering Samples
  • Remark 4.6
  • ...and 4 more