Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Neural Control Barrier Functions for Signal Temporal Logic Specifications with Input Constraints

Vaishnavi Jagabathula, Pushpak Jagtap

TL;DR

The paper tackles controller synthesis for continuous-time nonlinear systems under Signal Temporal Logic (STL) specifications with input constraints. It introduces a neural network–based Time-Varying Control Barrier Function (TVCBF) that co-designs a barrier and a controller to enforce STL semantics, while a validity condition provides formal guarantees across the state space. An iterative safe-set refinement and a finite-sample training scheme are developed to ensure differentiability and satisfy barrier conditions, supported by Lipschitz and LMIs-based regularization. The approach is validated on mobile robots, a pendulum, and a rotating spacecraft, demonstrating STL satisfaction and adherence to input bounds across diverse tasks. Overall, the framework offers a scalable, data-driven path to safety-critical STL satisfaction with formal assurances in continuous-time systems.

Abstract

Signal Temporal Logic (STL) provides a powerful framework to describe complex tasks involving temporal and logical behavior in dynamical systems. In this work, we address the problem of synthesizing controllers for continuous-time systems under STL specifications with input constraints. We propose a neural network-based framework for synthesizing time-varying control barrier functions (TVCBF) and their corresponding controllers for systems to fulfill STL specifications while respecting input constraints. We formulate barrier conditions incorporating the spatial and temporal logic of the given STL specification. Additionally, we introduce a validity condition to provide formal safety guarantees across the entire state space. Finally, we demonstrate the effectiveness of the proposed approach through several simulation studies considering different STL tasks.

Neural Control Barrier Functions for Signal Temporal Logic Specifications with Input Constraints

TL;DR

The paper tackles controller synthesis for continuous-time nonlinear systems under Signal Temporal Logic (STL) specifications with input constraints. It introduces a neural network–based Time-Varying Control Barrier Function (TVCBF) that co-designs a barrier and a controller to enforce STL semantics, while a validity condition provides formal guarantees across the state space. An iterative safe-set refinement and a finite-sample training scheme are developed to ensure differentiability and satisfy barrier conditions, supported by Lipschitz and LMIs-based regularization. The approach is validated on mobile robots, a pendulum, and a rotating spacecraft, demonstrating STL satisfaction and adherence to input bounds across diverse tasks. Overall, the framework offers a scalable, data-driven path to safety-critical STL satisfaction with formal assurances in continuous-time systems.

Abstract

Signal Temporal Logic (STL) provides a powerful framework to describe complex tasks involving temporal and logical behavior in dynamical systems. In this work, we address the problem of synthesizing controllers for continuous-time systems under STL specifications with input constraints. We propose a neural network-based framework for synthesizing time-varying control barrier functions (TVCBF) and their corresponding controllers for systems to fulfill STL specifications while respecting input constraints. We formulate barrier conditions incorporating the spatial and temporal logic of the given STL specification. Additionally, we introduce a validity condition to provide formal safety guarantees across the entire state space. Finally, we demonstrate the effectiveness of the proposed approach through several simulation studies considering different STL tasks.

Paper Structure

This paper contains 19 sections, 6 theorems, 23 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Preliminaries and Problem Formulation
  3. System Description
  4. Signal Temporal Logic (STL)
  5. Problem Formulation
  6. Time-varying Control Barrier Function
  7. Time-Varying Control Barrier Function
  8. TVCBF for STL Specifications
  9. Neural Network-based Time-Varying CBF (N-TVCBF)
  10. Training of N-TVCBF and Controller
  11. Neural Network Architecture
  12. Training of N-TVCBF and Controller
  13. Neural Network Architecture
  14. Training Algorithm with Formal Guarantees
  15. Simulation Results
  16. ...and 4 more sections

Key Result

Theorem 1

For a continuous-time control system $\Sigma$ in dyn_eq and a time-varying set $\mathcal{C}(t)$, suppose there exist a continuously differentiable function $\mathcal{B}:W\rightarrow \mathbb{R}$ and a controller $\textsl{g}:W\rightarrow U$ satisfying conditions cbf_1-cbf_3. Then, the system trajector

Figures (5)

  • Figure 1: Neural network architecture
  • Figure 2: Mecanum satisfying $\Phi_1$\ref{['phi_1']} with state trajectories starting at $[-1,-1]^\top$(blue), $[1.4,-0.3]^\top$(purple), N-TVCBF $\mathcal{B}_{\theta_1}(\mathbf{x}(t),t)$ and controller $\textsl{g}_{\theta_2}(\mathbf{x}(t),t)$ satisfying \ref{['cbf_1']}-\ref{['cbf_3']}, keeping control inputs within limits (dotted red lines)
  • Figure 3: Pendulum satisfying $\Phi_2$\ref{['phi_2']} with state trajectories starting at different initial states $[1.1,0.01]^\top$(blue), $[0.6,0.1]^\top$(purple), $[0.4,0.01]^\top$(yellow), N-TVCBF $\mathcal{B}_{\theta_1}(\mathbf{x}(t),t)$ and controller $\textsl{g}_{\theta_2}(\mathbf{x}(t),t)$ satisfying \ref{['cbf_1']}-\ref{['cbf_3']}, keeping control inputs within limits (dotted red lines)
  • Figure 4: Pendulum satisfying $\Phi_3$\ref{['phi_3']} with state trajectories starting at different initial states $[1.1,0.1]^\top$(blue), $[0.6,0.01]^\top$(brown), $[-1.1,0.01]^\top$(purple), $[-0.4,0.1]^\top$(orange), N-TVCBF $\mathcal{B}_{\theta_1}(\mathbf{x}(t),t)$ and controller $\textsl{g}_{\theta_2}(\mathbf{x}(t),t)$ satisfying \ref{['cbf_1']}-\ref{['cbf_3']}, keeping control inputs within limits (dotted red lines)
  • Figure 5: Spacecraft satisfying $\Phi_4$ with state trajectories starting at different initial states $[-0.02,-0.02,0.02]^\top$(blue), $[0,0,0]^\top$(brown), $[0.02,0.02,0.02]^\top$(purple), N-TVCBF $\mathcal{B}_{\theta_1}(\mathbf{x}(t),t)$ and controller $\textsl{g}_{\theta_2}(\mathbf{x}(t),t)$ satisfying \ref{['cbf_1']}-\ref{['cbf_3']}, keeping control inputs within limits (dotted red lines)

Theorems & Definitions (13)

  • Definition 1
  • Theorem 1
  • proof
  • Theorem 2
  • proof
  • Lemma 1
  • proof
  • Lemma 2
  • Theorem 3
  • proof
  • ...and 3 more