Neural Control Barrier Functions for Signal Temporal Logic Specifications with Input Constraints
Vaishnavi Jagabathula, Pushpak Jagtap

TL;DR
This paper introduces a neural network-based framework for synthesizing time-varying control barrier functions to ensure complex STL-specified tasks are safely achieved by dynamical systems under input constraints.
Contribution
It proposes a novel neural control barrier function approach that incorporates STL specifications and input constraints, with formal safety guarantees.
Findings
Successfully synthesizes controllers for STL tasks in simulations.
Ensures safety and task fulfillment under input constraints.
Demonstrates effectiveness on various dynamical systems.
Abstract
Signal Temporal Logic (STL) provides a powerful framework to describe complex tasks involving temporal and logical behavior in dynamical systems. This work addresses controller synthesis for continuous-time systems subject to STL specifications and 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 a fragment of STL specifications while respecting input constraints. We formulate barrier conditions incorporating the spatial and temporal logic of the given STL specification. We also incorporate a method to refine the time-varying set that satisfies the STL specification for the given input constraints. Additionally, we introduce a validity condition to provide formal safety guarantees across the entire state space. Finally, we demonstrate the effectiveness…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Adversarial Robustness in Machine Learning · Gene Regulatory Network Analysis
