Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Approximation-free Control for Signal Temporal Logic Specifications using Spatiotemporal Tubes

Ratnangshu Das, Subhodeep Choudhury, Pushpak Jagtap

TL;DR

The paper addresses the challenge of enforcing general STL specifications on unknown control-affine systems with disturbances. It introduces a spatiotemporal-tube (STT) framework that formulates STL constraints as a robust optimization problem, relaxes it to a scenario optimization program for offline tube construction, and derives a closed-form, approximation-free controller that guarantees STL satisfaction by keeping the system inside the STTs. The approach yields formal guarantees, scales to complex specifications, and demonstrates superior computational efficiency compared to MILP, MPC, CBF, and funnel-based methods across robotic and spacecraft case studies. This enables reliable, model-agnostic STL control with practical applicability to complex time-constrained tasks.

Abstract

This paper presents a spatiotemporal tube (STT)-based control framework for satisfying Signal Temporal Logic (STL) specifications in unknown control-affine systems. We formulate STL constraints as a robust optimization problem (ROP) and recast it as a scenario optimization program (SOP) to construct STTs with formal correctness guarantees. We also propose a closed-form control law that operates independently of the system dynamics, and ensures the system trajectory evolves within the STTs, thereby satisfying the STL specifications. The proposed approach is validated through case studies and comparisons with state-of-the-art methods, demonstrating superior computational efficiency, trajectory quality, and applicability to complex STL tasks.

Approximation-free Control for Signal Temporal Logic Specifications using Spatiotemporal Tubes

TL;DR

The paper addresses the challenge of enforcing general STL specifications on unknown control-affine systems with disturbances. It introduces a spatiotemporal-tube (STT) framework that formulates STL constraints as a robust optimization problem, relaxes it to a scenario optimization program for offline tube construction, and derives a closed-form, approximation-free controller that guarantees STL satisfaction by keeping the system inside the STTs. The approach yields formal guarantees, scales to complex specifications, and demonstrates superior computational efficiency compared to MILP, MPC, CBF, and funnel-based methods across robotic and spacecraft case studies. This enables reliable, model-agnostic STL control with practical applicability to complex time-constrained tasks.

Abstract

This paper presents a spatiotemporal tube (STT)-based control framework for satisfying Signal Temporal Logic (STL) specifications in unknown control-affine systems. We formulate STL constraints as a robust optimization problem (ROP) and recast it as a scenario optimization program (SOP) to construct STTs with formal correctness guarantees. We also propose a closed-form control law that operates independently of the system dynamics, and ensures the system trajectory evolves within the STTs, thereby satisfying the STL specifications. The proposed approach is validated through case studies and comparisons with state-of-the-art methods, demonstrating superior computational efficiency, trajectory quality, and applicability to complex STL tasks.
Paper Structure (13 sections, 3 theorems, 18 equations, 3 figures, 1 table)

This paper contains 13 sections, 3 theorems, 18 equations, 3 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries and Problem Formulation
  3. System Definition
  4. Signal Temporal Logic (STL)
  5. Spatiotemporal Tubes
  6. Problem Statement
  7. Construction of Spatiotemporal Tubes
  8. Controller Design and Theoretical Analysis
  9. Case Studies
  10. Omnidirectional Robot
  11. Rotating Rigid Spacecraft
  12. Comparison
  13. Conclusion and Future Work

Key Result

Theorem 3.2

$\mu(\lambda_1, \ldots, \lambda_n) := -\rho (x)$ with $x(\tau) = [\lambda_1 \gamma_{1,U}(c_{1,U},\tau) + (1 - \lambda_1)\gamma_{1,L}(c_{1,L},\tau), \ldots, \lambda_n \gamma_{n,U}(c_{n,U},\tau) + (1 - \lambda_n)\gamma_{n,L}(c_{n,L},\tau)]^\top$ for all $\tau \in [0,t_f]$, is Lipschitz continuous with

Figures (3)

  • Figure 1: Time complexity
  • Figure 2: (a) Trajectory (b) Generated STTs for mobile robot.
  • Figure 3: (a) System trajectory and (b), (c), (d) are generated STTs for Spacecraft Case Study.

Theorems & Definitions (14)

  • Remark 2.1
  • Definition 2.2: STTs for STL Task
  • Remark 2.3
  • Remark 3.1
  • Theorem 3.2
  • Proof 3.3
  • Theorem 3.4
  • Proof 3.5
  • Remark 3.6
  • Remark 3.7
  • ...and 4 more