Temporal Logic Control for Nonlinear Stochastic Systems Under Unknown Disturbances

TL;DR

This work tackles the synthesis of robust controllers for discrete-time nonlinear systems with unknown disturbance distributions under $\mathrm{LTL}_f$ specifications. It introduces a data-driven, abstraction-based framework that learns a high-confidence Uncertain MDP (UMDP) with convex polytope transition uncertainty via a two-layer state discretization and disturbance-support learning, enabling tighter guarantees than traditional IMDP approaches. A tailored robust dynamic programming algorithm operates on the product of the UMDP with the $\mathrm{LTL}_f$ automaton, yielding provable bounds on the satisfaction probability and scalable synthesis. Empirical results across multiple nonlinear and multi-dimensional systems show substantial improvements in sample efficiency, bound tightness, and computation time compared to the state of the art. The approach thus offers a practical pathway to reliable, data-driven control under unknown disturbances for complex dynamical systems.

Abstract

In this paper, we present a novel framework to synthesize robust strategies for discrete-time nonlinear systems with random disturbances that are unknown, against temporal logic specifications. The proposed framework is data-driven and abstraction-based: leveraging observations of the system, our approach learns a high-confidence abstraction of the system in the form of an uncertain Markov decision process (UMDP). The uncertainty in the resulting UMDP is used to formally account for both the error in abstracting the system and for the uncertainty coming from the data. Critically, we show that for any given state-action pair in the resulting UMDP, the uncertainty in the transition probabilities can be represented as a convex polytope obtained by a two-layer state discretization and concentration inequalities. This allows us to obtain tighter uncertainty estimates compared to existing approaches, and guarantees efficiency, as we tailor a synthesis algorithm exploiting the structure of this UMDP. We empirically validate our approach on several case studies, showing substantially improved performance compared to the state-of-the-art.

Figures (10)

• Figure 1: Illustration of the sets in Def. \ref{['def:robust_mdp']}. $C(s,a) = \{q_1,q_2,q_3,q_4\}$, and each $q_i$ contains $4$ states. The probability that the successor state of $s=J(r)$ under action $a$ will be in $C(s,a)$ is higher than $1-\epsilon$. Note that the reachable sets corresponding to $\boldsymbol{\hat{w}}^{(2)}$ and $\boldsymbol{\hat{w}}^{(3)}$ are contained in $q_3$ and $q_4$, respectively, but no single region in the fine partition contains them completely.
• Figure 2: Naïve IMDP
• Figure 3: IMDP with learned support
• Figure 4: UMDP \ref{['def:umdp abstraction']}
• Figure 6: Pendulum ($N=5\times10^4$)

Theorems & Definitions (26)

• Definition 3.1: Uncertain MDP
• Definition 3.2: Interval MDP
• Proposition 4.1
• Proposition 4.2
• proof
• Remark 4.3
• Proposition 4.4: Confidence Region
• Definition 4.5: UMDP Abstraction
• Theorem 4.6: Soundness of UMDP Abstraction
• proof