Robust STL Control Synthesis under Maximal Disturbance Sets

TL;DR

The paper addresses the problem of synthesizing controllers that are robust to unknown disturbances by jointly maximizing the disturbance bound and ensuring strict satisfaction of a time-bounded STL specification for a general nonlinear system. It introduces disturbance-robust STL semantics and a constructive algorithm that concatenates Backwards Reachable Sets derived from Hamilton-Jacobi-Isaacs reachability to compute maximally disturbance-robust controllers, including under-approximations that make the problem tractable. The method is demonstrated through simulations, including a planar AUV and a more complex AUV inspection scenario, showing how larger disturbance sets can be accommodated without violating the STL requirements and providing quantified disturbance robustness. The contributions offer a principled framework for balance between disturbance tolerance and specification satisfaction, with soundness proofs and practical insights into computational trade-offs, enabling robust autonomous operation under uncertain environmental forces.

Abstract

This work addresses maximally robust control synthesis under unknown disturbances. We consider a general nonlinear system, subject to a Signal Temporal Logic (STL) specification, and wish to jointly synthesize the maximal possible disturbance bounds and the corresponding controllers that ensure the STL specification is satisfied under these bounds. Many works have considered STL satisfaction under given bounded disturbances. Yet, to the authors' best knowledge, this is the first work that aims to maximize the permissible disturbance set and find the corresponding controllers that ensure satisfying the STL specification with maximum disturbance robustness. We extend the notion of disturbance-robust semantics for STL, which is a property of a specification, dynamical system, and controller, and provide an algorithm to get the maximal disturbance robust controllers satisfying an STL specification using Hamilton-Jacobi reachability. We show its soundness and provide a simulation example with an Autonomous Underwater Vehicle (AUV).

Figures (3)

• Figure 1: An illustrative reference trajectory (top) and the simulated trajectories from our method (bottom) of an AUV required, to be in $A$ between $7$ and $8$ seconds. The top scenario is more space- and time-robust while the bottom scenario is more disturbance-robust. Solid lines indicate the undisturbed trajectory (using the maximal disturbance robust controllers), the dashed line with the obtained maximal disturbance set.
• Figure 2: Concatenation of reachable sets. $(t_1,t_2)$ indicates between which times the optimal controller corresponding to the BRS will be active. a) for Always, the reachable sets should intersect at $t_5$ and contain a stay-in reachability computation from $t_5$ to $t_4$ (blue). The only valid path is $(\mathcal{D}_0,0\mathrel{\!\!:\!\!}5),(\mathcal{D}_0,5\mathrel{\!\!:\!\!}10)$, b) for Eventually, $A$ can be met at $t_4$ or $t_5$ (solid and dashed lines). The optimal valid path is $(\mathcal{D}_0,0\mathrel{\!\!:\!\!}4),(\mathcal{D}_1,4\mathrel{\!\!:\!\!}10)$, $\mathcal{D}^* = \mathcal{D}_0$, c) for Until, we consider three set concatenations. Blue sets need strict satisfaction at $\underline{I}$, red ensures $A\rightarrow B$ for any $t\in I$ and green ensures $B\rightarrow \mathcal{X}_f$ for that same $t$.
• Figure 3: An AUV subjected to an STL specification after finding the maximum permissible disturbance. The system is guaranteed to satisfy $\phi$$\forall \mathcal{D} \subseteq \mathcal{D}^*$. We show the maximally disturbed and undisturbed case.

Theorems & Definitions (10)

• Definition 1
• Definition 2: Fragment of Signal Temporal Logic
• Definition 3: Disturbance-Robust STL
• Remark 1
• Lemma 1: Disturbance-Robust Recursive Semantics
• proof : Proof Sketch
• Proposition 1
• Remark 2
• Theorem 1
• proof