GradSTL: Comprehensive Signal Temporal Logic for Neurosymbolic Reasoning and Learning
By: Mark Chevallier , Filip Smola , Richard Schmoetten and more
Potential Business Impact:
Teaches computers to follow complex rules.
We present GradSTL, the first fully comprehensive implementation of signal temporal logic (STL) suitable for integration with neurosymbolic learning. In particular, GradSTL can successfully evaluate any STL constraint over any signal, regardless of how it is sampled. Our formally verified approach specifies smooth STL semantics over tensors, with formal proofs of soundness and of correctness of its derivative function. Our implementation is generated automatically from this formalisation, without manual coding, guaranteeing correctness by construction. We show via a case study that using our implementation, a neurosymbolic process learns to satisfy a pre-specified STL constraint. Our approach offers a highly rigorous foundation for integrating signal temporal logic and learning by gradient descent.
Similar Papers
Trajectory Planning with Signal Temporal Logic Costs using Deterministic Path Integral Optimization
Systems and Control
Teaches robots to follow complex instructions precisely.
TeLoGraF: Temporal Logic Planning via Graph-encoded Flow Matching
Robotics
Teaches robots to follow complex instructions.
Cumulative-Time Signal Temporal Logic
Logic in Computer Science
Lets computers track how long things happen.