Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Control Barrier Functions for the Full Class of Signal Temporal Logic Tasks using Spatiotemporal Tubes

Ratnangshu Das, Subhodeep Choudhury, Pushpak Jagtap

TL;DR

This work presents a unified framework to synthesize time-varying control barrier functions (TV-CBFs) capable of enforcing the full class of Signal Temporal Logic (STL) specifications via Spatiotemporal Tubes (STTs). By formulating STT synthesis as a robust optimization problem and solving it through a scenario optimization approach, the method guarantees that the resulting tube captures the STL task and yields a TV-CBF that enforces forward invariance under a safety-preserving controller. The STT is parameterized with spherical cross-sections, reducing computational complexity, and is used to construct a TV-CBF with a quadratic program to guarantee STL satisfaction for the system dynamics. Case studies on a differential-drive robot and a quadrotor demonstrate computational efficiency and scalability advantages over MILP, MPC, CBF, and PPC baselines, while handling complex STL specifications. The framework offers a practical, verification-friendly path to safety-critical STL-guided control in robotics and autonomous systems.

Abstract

This paper introduces a new framework for synthesizing time-varying control barrier functions (TV-CBFs) for general Signal Temporal Logic (STL) specifications using spatiotemporal tubes (STT). We first formulate the STT synthesis as a robust optimization problem (ROP) and solve it through a scenario optimization problem (SOP), providing formal guarantees that the resulting tubes capture the given STL specifications. These STTs are then used to construct TV-CBFs, ensuring that under any control law rendering them invariant, the system satisfies the STL tasks. We demonstrate the framework through case studies on a differential-drive mobile robot and a quadrotor, and provide a comparative analysis showing improved efficiency over existing approaches.

Control Barrier Functions for the Full Class of Signal Temporal Logic Tasks using Spatiotemporal Tubes

TL;DR

This work presents a unified framework to synthesize time-varying control barrier functions (TV-CBFs) capable of enforcing the full class of Signal Temporal Logic (STL) specifications via Spatiotemporal Tubes (STTs). By formulating STT synthesis as a robust optimization problem and solving it through a scenario optimization approach, the method guarantees that the resulting tube captures the STL task and yields a TV-CBF that enforces forward invariance under a safety-preserving controller. The STT is parameterized with spherical cross-sections, reducing computational complexity, and is used to construct a TV-CBF with a quadratic program to guarantee STL satisfaction for the system dynamics. Case studies on a differential-drive robot and a quadrotor demonstrate computational efficiency and scalability advantages over MILP, MPC, CBF, and PPC baselines, while handling complex STL specifications. The framework offers a practical, verification-friendly path to safety-critical STL-guided control in robotics and autonomous systems.

Abstract

This paper introduces a new framework for synthesizing time-varying control barrier functions (TV-CBFs) for general Signal Temporal Logic (STL) specifications using spatiotemporal tubes (STT). We first formulate the STT synthesis as a robust optimization problem (ROP) and solve it through a scenario optimization problem (SOP), providing formal guarantees that the resulting tubes capture the given STL specifications. These STTs are then used to construct TV-CBFs, ensuring that under any control law rendering them invariant, the system satisfies the STL tasks. We demonstrate the framework through case studies on a differential-drive mobile robot and a quadrotor, and provide a comparative analysis showing improved efficiency over existing approaches.
Paper Structure (14 sections, 5 theorems, 32 equations, 4 figures, 1 table)

This paper contains 14 sections, 5 theorems, 32 equations, 4 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries and Problem Formulation
  3. System Definition
  4. Signal Temporal Logic (STL)
  5. Time-varying Control Barrier Functions
  6. Problem Formulation
  7. Spatiotemporal Tubes
  8. Construction of Spatiotemporal Tubes
  9. STT-CBF Framework
  10. Case Studies
  11. Differential-Drive Mobile Robot
  12. Quadrotor in a 3D Environment
  13. Comparison
  14. Conclusion

Key Result

Theorem 2.4

If $u(t,x) \in {\mathbf{U}}_a(t,x)$ is locally Lipschitz continuous in $x$ and piecewise continuous in $t$ and the (consequently) unique solutions to eqn:sysdyn are defined over the time interval $[0, t_f]$. Then the set ${\mathcal{C}}(t)$ is forward invariant for the control law $u(t,x)$ if $b(t, x

Figures (4)

  • Figure 1: An omnidirectional mobile robot satisfying the STL task ${\lozenge}_{[0,6]} T \land {\Box}_{[0,6]} \neg O$, with the target $T$ (green) and obstacle $O$ (red). (a) The constructed STT (blue). (b)-(d) The 0-superlevel set of the TV-CBF (blue circle) and the controlled system trajectory (black line) at different time instances.
  • Figure 2: (a) STT (blue) and (b) the corresponding trajectory (black) for the differential-drive robot. The vehicle starts from $S$ (blue), visits $T_1$ or $T_2$ (cyan), then reaches $G$ (green), while avoiding obstacle $O$ (red) throughout the mission.
  • Figure 3: Quadrotor trajectory for the 3D surveillance task. The vehicle starts from $S$ (green), repeatedly visits $T_1$, $T_2$, and $T_3$ (cyan) in sequence, then reaches $G$ (green), while avoiding obstacle $O$ (red) throughout the mission. (a)–(d) show the vehicle trajectory at different time instances.
  • Figure 4: Comparison of trajectories obtained using the proposed STT-CBF framework, STT-based controller, MILP, MPC, CBF, and Funnel approaches for the four benchmark tasks (stlcg-1, stlcg-2, stlfrag-1, and stlfrag-2).

Theorems & Definitions (16)

  • Definition 2.1: Candidate Control Barrier Function CBF_STL
  • Definition 2.2: Valid Control Barrier Function
  • Definition 2.3: Forward Invariance CBF_STL
  • Theorem 2.4: glotfelter2017nonsmooth
  • Definition 3.1: STT for STL Specification
  • Remark 3.2
  • Lemma 3.3
  • Proof 3.4
  • Theorem 3.5
  • Proof 3.6
  • ...and 6 more