Document Open Access Logo

GradSTL: Comprehensive Signal Temporal Logic for Neurosymbolic Reasoning and Learning

Authors Mark Chevallier , Filip Smola , Richard Schmoetten , Jacques D. Fleuriot

PDF

File

Thumbnail PDF
PDF
LIPIcs.TIME.2025.6.pdf
  • Filesize: 0.9 MB
  • 14 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Computing methodologies → Neural networks
Keywords
  • Signal temporal logic
  • spatio-temporal reasoning
  • neurosymbolic learning

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get BibTex

Mark Chevallier, Filip Smola, Richard Schmoetten, and Jacques D. Fleuriot. GradSTL: Comprehensive Signal Temporal Logic for Neurosymbolic Reasoning and Learning. In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 6:1-6:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.TIME.2025.6

Author Details

Mark Chevallier
  • School of Engineering, University of Edinburgh, UK
Filip Smola
  • School of Informatics, University of Edinburgh, UK
Richard Schmoetten
  • School of Informatics, University of Edinburgh, UK
Jacques D. Fleuriot
  • School of Informatics, University of Edinburgh, UK

Acknowledgements

We thank the referees for their feedback. This research was funded by the Edinburgh Laboratory for Integrated Artificial Intelligence (ELIAI) EPSRC (EP/W002876/1), by the Fonds National de la Recherche, Luxembourg (AFR 15671644), and by the Legal & General Group (research grant to establish the independent Advanced Care Research Centre at University of Edinburgh). Legal & General had no role in conducting the study, interpretation or the decision to submit for publication. The views expressed are those of the authors and not necessarily those of Legal & General. The Artificial Intelligence and its Applications Institute (AIAI) provided support for attending TIME 2025.

References

  1. E Abele, F Haehn, M Pischan, and F Herr. Time optimal path planning for industrial robots using STL data files. Procedia Cirp, 55:6-11, 2016. URL: https://doi.org/10.1016/j.procir.2016.08.038.
  2. Yashwanth Annpureddy, Che Liu, Georgios Fainekos, and Sriram Sankaranarayanan. [s-taliro: A tool for temporal logic falsification for hybrid systems]. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 254-257. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-19835-9_21.
  3. Nikos Arechiga. Specifying safety of autonomous vehicles in signal temporal logic. In 2019 IEEE Intelligent Vehicles Symposium (IV), pages 58-63. IEEE, 2019. URL: https://doi.org/10.1109/IVS.2019.8813875.
  4. Eugene Asarin, Alexandre Donzé, Oded Maler, and Dejan Nickovic. Parametric identification of temporal properties. In Runtime Verification: Second International Conference, RV 2011, San Francisco, CA, USA, September 27-30, 2011, Revised Selected Papers 2, pages 147-160. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-29860-8_12.
  5. Mark Chevallier, Filip Smola, Richard Schmoetten, and Jacques D. Fleuriot. Formally verified neurosymbolic trajectory learning via tensor-based linear temporal logic on finite traces, 2025. arXiv preprint arXiv:2501.13712. URL: https://doi.org/10.48550/arXiv.2501.13712.
  6. Marco Cuturi and Mathieu Blondel. Soft-dtw: a differentiable loss function for time-series. In Doina Precup and Yee Whye Teh, editors, Proceedings of the 34th International Conference on Machine Learning, ICML 2017, Sydney, NSW, Australia, 6-11 August 2017, volume 70 of Proceedings of Machine Learning Research, pages 894-903. PMLR, 2017. URL: https://doi.org/10.48550/arXiv.1703.01541.
  7. Alexandre Donzé. Breach, a toolbox for verification and parameter synthesis of hybrid systems. In Computer Aided Verification: 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings 22, pages 167-170. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14295-6_17.
  8. Thomas Flinkow, Barak A. Pearlmutter, and Rosemary Monahan. Comparing differentiable logics for learning with logical constraints. Sci. Comput. Program., 244:103280, 2025. URL: https://doi.org/10.1016/j.scico.2025.103280.
  9. Florian Haftmann and Lukas Bulwahn. Code generation from Isabelle/HOL theories, 2021. Found online at https://isabelle.in.tum.de/doc/codegen.pdf, last checked April 24 2025.
  10. Florian Haftmann and Tobias Nipkow. Code generation via higher-order rewrite systems. In Matthias Blume, Naoki Kobayashi, and Germán Vidal, editors, Functional and Logic Programming, pages 103-117, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-12251-4_9.
  11. Parv Kapoor, Kazuki Mizuta, Eunsuk Kang, and Karen Leung. STLCG++: A Masking Approach for Differentiable Signal Temporal Logic Specification, 2025. URL: https://doi.org/10.48550/arXiv.2501.04194.
  12. Diederik P. Kingma and Jimmy Ba. Adam: A method for stochastic optimization. In Yoshua Bengio and Yann LeCun, editors, 3rd International Conference on Learning Representations, ICLR 2015, San Diego, CA, USA, May 7-9, 2015, Conference Track Proceedings, 2015. URL: https://doi.org/10.48550/arXiv.1412.6980.
  13. Karen Leung, Nikos Aréchiga, and Marco Pavone. Backpropagation for parametric STL. In 2019 IEEE Intelligent Vehicles Symposium (IV), pages 185-192. IEEE, 2019. URL: https://doi.org/10.1109/IVS.2019.8814167.
  14. Karen Leung, Nikos Aréchiga, and Marco Pavone. Backpropagation through signal temporal logic specifications: Infusing logical structure into gradient-based methods. The International Journal of Robotics Research, 42(6):356-370, 2023. URL: https://doi.org/10.1177/02783649221082115.
  15. Danyang Li, Mingyu Cai, Cristian-Ioan Vasile, and Roberto Tron. TLINet: Differentiable Neural Network Temporal Logic Inference, 2024. arXiv preprint arXiv:2405.06670. URL: https://doi.org/10.48550/arXiv.2405.06670.
  16. Xiao Li, Guy Rosman, Igor Gilitschenski, Jonathan A. DeCastro, Cristian Ioan Vasile, Sertac Karaman, and Daniela Rus. Differentiable logic layer for rule guided trajectory prediction. In Jens Kober, Fabio Ramos, and Claire J. Tomlin, editors, 4th Conference on Robot Learning, CoRL 2020, 16-18 November 2020, Virtual Event / Cambridge, MA, USA, volume 155 of Proceedings of Machine Learning Research, pages 2178-2194. PMLR, PMLR, 2020. URL: https://proceedings.mlr.press/v155/li21b.html.
  17. Wenliang Liu, Wei Xiao, and Calin Belta. Learning robust and correct controllers from signal temporal logic specifications using BarrierNet. In 2023 62nd IEEE Conference on Decision and Control (CDC), pages 7049-7054. IEEE, 2023. URL: https://doi.org/10.1109/CDC49753.2023.10383857.
  18. Oded Maler and Dejan Nickovic. Monitoring temporal properties of continuous signals. In International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, pages 152-166. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30206-3_12.
  19. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: a proof assistant for higher-order logic, volume 2283. Springer Science & Business Media, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  20. Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Köpf, Edward Z. Yang, Zachary DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala. Pytorch: An imperative style, high-performance deep learning library. In Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d'Alché-Buc, Emily B. Fox, and Roman Garnett, editors, Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada, volume 32, pages 8024-8035, 2019. URL: https://proceedings.neurips.cc/paper/2019/hash/bdbca288fee7f92f2bfa9f7012727740-Abstract.html.
  21. Vasumathi Raman, Alexandre Donzé, Dorsa Sadigh, Richard M Murray, and Sanjit A Seshia. Reactive synthesis from signal temporal logic specifications. In Proceedings of the 18th international conference on hybrid systems: Computation and control, pages 239-248, 2015. URL: https://doi.org/10.1145/2728606.2728628.
  22. Wei Xiao, Ramin Hasani, Xiao Li, and Daniela Rus. Barriernet: A safety-guaranteed layer for neural networks, 2021. arXiv preprint arXiv:2111.11277. URL: https://doi.org/10.48550/arXiv.2111.11277.
  23. Ruixuan Yan, Agung Julius, Maria Chang, Achille Fokoue, Tengfei Ma, and Rosario Uceda-Sosa. STONE: Signal temporal logic neural network for time series classification. In 2021 International Conference on Data Mining Workshops (ICDMW), pages 778-787. IEEE, 2021. URL: https://doi.org/10.1109/ICDMW53433.2021.00101.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact