GradSTL: Comprehensive Signal Temporal Logic for Neurosymbolic Reasoning and Learning

TL;DR

GradSTL introduces a fully verified, tensor-based implementation of signal temporal logic that seamlessly integrates with neurosymbolic learning, enabling gradient-based satisfaction of STL constraints.

Contribution

It provides the first comprehensive, formally verified, and automatically generated STL implementation compatible with neurosymbolic learning frameworks.

Findings

Successfully evaluates any STL constraint over any signal.

Guarantees correctness through formal proofs of soundness and derivative correctness.

Enables neurosymbolic learning to satisfy STL constraints via gradient descent.

Abstract

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.