2026-09-17T01:51:56Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:24452 2026-09-05T18:56:17Z ddc:004 open_access

GradSTL: Comprehensive Signal Temporal Logic for Neurosymbolic Reasoning and Learning Chevallier, Mark Smola, Filip Schmoetten, Richard Fleuriot, Jacques D. Signal temporal logic spatio-temporal reasoning neurosymbolic learning 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Mark Chevallier and Filip Smola and Richard Schmoetten and Jacques D. Fleuriot 2025 Is Part Of LIPIcs, Volume 355, 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TIME.2025.6 urn:nbn:de:0030-drops-244528 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.6 eng https://creativecommons.org/licenses/by/4.0/legalcode