Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Continuous-time control synthesis under nested signal temporal logic specifications

Pian Yu, Xiao Tan, Dimos V. Dimarogonas

TL;DR

The paper tackles continuous-time control synthesis for nonlinear systems under nested STL specifications. It introduces the signal temporal logic tree (sTLT) to convert temporal logic satisfaction into a sequence of set-invariance constraints and couples it with time-varying control barrier functions (CBFs) implemented via an online, event-triggered update scheme. Theoretical results establish equivalence or under-approximation between STL formulas and their sTLT representations, enabling a principled online CBF-based controller that solves QPs to ensure correctness. Case studies on a single-integrator and a unicycle validate the approach, illustrate online feasibility, and highlight the role of branch selection in handling disjunctions within nested specifications.

Abstract

In this work, we propose a novel approach for the continuous-time control synthesis of nonlinear systems under nested signal temporal logic (STL) specifications. While the majority of existing literature focuses on control synthesis for STL specifications without nested temporal operators, addressing nested temporal operators poses a notably more challenging scenario and requires new theoretical advancements. Our approach hinges on the concepts of signal temporal logic tree (sTLT) and control barrier function (CBF). Specifically, we detail the construction of an sTLT from a given STL formula and a continuous-time dynamical system, the sTLT semantics (i.e., satisfaction condition), and the equivalence or under-approximation relation between sTLT and STL. Leveraging the fact that the satisfaction condition of an sTLT is essentially keeping the state within certain sets during certain time intervals, it provides explicit guidelines for the CBF design. The resulting controller is obtained through the utilization of an online CBF-based program coupled with an event-triggered scheme for online updating the activation time interval of each CBF, with which the correctness of the system behavior can be established by construction. We demonstrate the efficacy of the proposed method for single-integrator and unicycle models under nested STL formulas.

Continuous-time control synthesis under nested signal temporal logic specifications

TL;DR

The paper tackles continuous-time control synthesis for nonlinear systems under nested STL specifications. It introduces the signal temporal logic tree (sTLT) to convert temporal logic satisfaction into a sequence of set-invariance constraints and couples it with time-varying control barrier functions (CBFs) implemented via an online, event-triggered update scheme. Theoretical results establish equivalence or under-approximation between STL formulas and their sTLT representations, enabling a principled online CBF-based controller that solves QPs to ensure correctness. Case studies on a single-integrator and a unicycle validate the approach, illustrate online feasibility, and highlight the role of branch selection in handling disjunctions within nested specifications.

Abstract

In this work, we propose a novel approach for the continuous-time control synthesis of nonlinear systems under nested signal temporal logic (STL) specifications. While the majority of existing literature focuses on control synthesis for STL specifications without nested temporal operators, addressing nested temporal operators poses a notably more challenging scenario and requires new theoretical advancements. Our approach hinges on the concepts of signal temporal logic tree (sTLT) and control barrier function (CBF). Specifically, we detail the construction of an sTLT from a given STL formula and a continuous-time dynamical system, the sTLT semantics (i.e., satisfaction condition), and the equivalence or under-approximation relation between sTLT and STL. Leveraging the fact that the satisfaction condition of an sTLT is essentially keeping the state within certain sets during certain time intervals, it provides explicit guidelines for the CBF design. The resulting controller is obtained through the utilization of an online CBF-based program coupled with an event-triggered scheme for online updating the activation time interval of each CBF, with which the correctness of the system behavior can be established by construction. We demonstrate the efficacy of the proposed method for single-integrator and unicycle models under nested STL formulas.
Paper Structure (22 sections, 6 theorems, 36 equations, 7 figures, 4 algorithms)

This paper contains 22 sections, 6 theorems, 36 equations, 7 figures, 4 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries and Problem Formulation
  3. Signal temporal logic
  4. Reachability operators
  5. Time-varying control barrier functions
  6. Problem formulation
  7. Solving the Control Synthesis Problem
  8. sTLT and its construction
  9. sTLT semantics
  10. Relations between $\mathcal{T}_{\hat{\varphi}}$ and $\hat{\varphi}$ ($\varphi$)
  11. Design of CBFs
  12. Time encoding for the sTLT
  13. CBF design for each temporal fragment
  14. The overall algorithm
  15. Nested STL formulas that contain no $\vee$ operator
  16. ...and 7 more sections

Key Result

Lemma 1

Given the system (x0) and the STL predicate $\mu_1$, one has where $\mathbb{S}_{\mathsf{F}_{[a, b]}\mu_1}$ and $\mathbb{S}_{\mathsf{G}_{[a, b]}\mu_1}$ are the satisfying sets for $\mathsf{F}_{[a, b]}\mu_1$ and $\mathsf{G}_{[a, b]}\mu_1$, respectively.

Figures (7)

  • Figure 1: The sTLT construction for: (a) $\varphi_1\wedge \varphi_2$; (b) $\varphi_1\vee \varphi_2$; (c) $\mathsf{F}_{[a, b]}\varphi_1$; (d) $\mathsf{G}_{[a, b]}\varphi_1$. The circles denote the operator nodes and the rectangles denote the set nodes.
  • Figure 2: The sTLT $\mathcal{T}_{\hat{\varphi}}$ for the nested STL formula $\varphi=\mathsf{F}_{[0, 15]}(\mathsf{G}_{[2, 10]}\mu_1 \vee \mu_2 \mathsf{U}_{[5, 10]}\mu_3)$.
  • Figure 3: The compressed tree $\mathcal{T}^c$ for the sTLT $\mathcal{T}_{\hat{\varphi}}$ plotted in Fig. \ref{['Fig:example']}.
  • Figure 4: Four trajectories of a mobile robot with single integrator dynamics are synthesized using the proposed method under the STL specification $\varphi=\mathsf{F}_{[0, 15]}(\mathsf{G}_{[2, 10]}\mu_1 \vee \mu_2 \mathsf{U}_{[5, 10]}\mu_3)$. Two different starting positions (marked in circles) are tested and every trajectory satisfies the STL specification $\varphi$. It is observed that the robot starts its voyage from $0$s and approaches the regions of interest without any stop. This was enabled by the design of the nominal controller and the online updates of the start time intervals of the set nodes. For the case that branch $\{ {\bm p}_2, {\bm p}_3\}$ is chosen, we note that the trajectories leave $\mathbb{X}_9$ after reaching it. This behavior is due to the approximation gap as we require the trajectories to stay inside $\mathbb{X}_8$ after reaching $\mathbb{X}_9$ for the constructed sTLT.
  • Figure 5: Four trajectories of a mobile robot with unicycle dynamics are synthesised using the proposed method under the STL specification $\varphi=\mathsf{F}_{[0, 15]}(\mathsf{G}_{[2, 10]}\mu_1 \vee \mu_2 \mathsf{U}_{[5, 10]}\mu_3)$. Two different starting configurations (marked in circles) are tested and every trajectory satisfies the STL specification $\varphi$. It is observed that the robot first adjusts its orientation and then starts to approach regions of interest without any stop. For the case that branch $\{ {\bm p}_2, {\bm p}_3\}$ is chosen, we also see that the trajectories leave $\mathbb{X}_9$ after reaching it.
  • ...and 2 more figures

Theorems & Definitions (40)

  • Definition 1: STL semantics raman2015reactive
  • Definition 2
  • Definition 3
  • Definition 4
  • Lemma 1: chen2018
  • Definition 5
  • Definition 6: CBF ames2016control
  • Definition 7: Nested STL formula
  • Definition 8: sTLT
  • Definition 9: Desired form
  • ...and 30 more