research-article

Backpropagation through signal temporal logic specifications: : Infusing logical structure into gradient-based methods

Authors:

Karen Leung, Nikos Aréchiga, Marco PavoneAuthors Info & Claims

The International Journal of Robotics Research, Volume 42, Issue 6

Pages 356 - 370

https://doi.org/10.1177/02783649221082115

Published: 01 May 2023 Publication History

Abstract

This paper presents a technique, named STLCG, to compute the quantitative semantics of Signal Temporal Logic (STL) formulas using computation graphs. STLCG provides a platform which enables the incorporation of logical specifications into robotics problems that benefit from gradient-based solutions. Specifically, STL is a powerful and expressive formal language that can specify spatial and temporal properties of signals generated by both continuous and hybrid systems. The quantitative semantics of STL provide a robustness metric, that is, how much a signal satisfies or violates an STL specification. In this work, we devise a systematic methodology for translating STL robustness formulas into computation graphs. With this representation, and by leveraging off-the-shelf automatic differentiation tools, we are able to efficiently backpropagate through STL robustness formulas and hence enable a natural and easy-to-use integration of STL specifications with many gradient-based approaches used in robotics. Through a number of examples stemming from various robotics applications, we demonstrate that STLCG is versatile, computationally efficient, and capable of incorporating human-domain knowledge into the problem formulation.

References

[1]

Adel T, Ghahramani Z, and Weller A (2018) Discovering interpretable representations for both deep generative and discriminative models. In: Proceedings of the 35th International Conference on Machine Learning, Stockholm Sweden, 10–15 July 2018.

[2]

Asarin E, Donzé A, and Maler O, et al. (2012) Parametric identification of temporal properties. Runtime Verification: 147–160. In: International Conference on Runtime Verification, 25–28 September 2012, Istanbul, Turkey.

[3]

Baier C and Katoen JP (2008) Principles of Model Checking. Cambridge, MA: MIT Press.

Digital Library

[4]

Bartocci E, Deshmukh J, and Donzé A, et al. (2018) Specification-based Monitoring of Cyber-Physical Systems: A Survey on Theory, Tools and Applications. Berlin, Germany: Springer, pp. 135–175.

[5]

Doersch C (2016) Tutorial on variational autoencoders. Available at: https://arxiv.org/abs/1606.05908.

[6]

Fainekos G, Sankaranarayanan S, and Ueda K, et al. (2012) Verification of automotive control applications using S-TaLiRo. In: American Control Conference, Montreal, QC, 27–29 June 2012.

[7]

Fainekos GE, Girard A, and Kress-Gazit H, et al. (2008) Temporal logic motion planning for dynamic robots. Automatica 45(2): 343–352.

[8]

Finucane C, Jing G, and Kress-Gazit H (2010) LTLMoP: Experimenting with language, temporal logic and robot control. In: IEEE/RSJ International Conference on Intelligent Robots & Systems, Taipei, Taiwan, 18–22 October 2010.

[9]

Gers FA, Schmidhuber J, and Cummins F (1999) Learning to forget: continual prediction with LSTM. In: International Conference on Artificial Neural Networks, Edinburgh, UK, 7–10 September 1999.

[10]

Hochreiter S and Schmidhuber J (1997) Long Short-Term Memory. Cambridge, MA: Neural Computation.

Digital Library

[11]

Jang E, Gu S, and Poole B (2017) Categorial reparameterization with gumbel-softmax. In: International Conference on Learning Representations, Toulon, France, 24–26 April 2017.

[12]

Kingma DP and Welling M (2013) Auto-encoding variational bayes. Available at: https://arxiv.org/abs/1312.6114.

[13]

Kress-Gazit H, Lahijanian M, and Raman V (2018) Synthesis for robots: Guarantees and feedback for robot behavior. Annual Review of Control, Robotics, and Autonomous Systems 1: 211–236.

[14]

Liu W, Mehdipour N, and Belta C (2021) Recurrent neural network controllers for signal temporal logic specifications subject to safety constraints. IEEE Control Systems Letters 6: 91–96.

[15]

Ma M, Gao J, and Feng L, et al. (2020) STLnet: Signal temporal logic enforced multivariate recurrent neural networks. In: Conference on Neural Information Processing Systems, Vancouver, BC, 6–12 December 2020.

[16]

Maler O and Nickovic D (2004) Monitoring temporal properties of continuous signals. In: Proceeding International Symp. Formal Techniques in Real-Time and Fault-Tolerant Systems, Formal Modeling and Analysis of Timed Systems, Grenoble, UK, 22–24 September 2004.

[17]

Mehdipour N, Vasile CI, and Belta C (2019) Arithmetic-geometric mean robustness for control from signal temporal logic specifications. In: American Control Conference, Philadelphia, PA, 10–12 July 2019.

[18]

Mehr N, Sadigh D, and Horowitz R, et al. (2017) Stochastic predictive freeway ramp metering from signal temporal logic specifications. In: American Control Conference, 24–26 May 2017, Seattle, WA.

[19]

Pant YV, Abbas H, and Mangharam R (2017) Smooth Operator: Control using the smooth robustness of temporal logic. In: IEEE Conf. Control Technology and Applications, Waimea, HI, 27–30 August 2017.

[20]

Paszke A, Gross S, and Chintala S, et al. (2017) Automatic differentiation in PyTorch. In: Conference on Neural Information Processing Systems - Autodiff Workshop, 4–9 December 2017, Long Beach, CA.

[21]

Pnueli A (1977) The temporal logic of programs. In: IEEE Symp. on Foundations of Computer Science, Washington, DC, 30 September–31 October 1977.

[22]

Puranic AG, Deshmukh JV, and Nikolaidis S (2020) Learning from demonstrations using signal temporal logic. In: Conference on Robot Learning, 16–18 November 2020.

[23]

Raman V, Donze A, and Maasoumy M, et al. (2014) Model predictive control with signal temporal logic specifications. In: Proceeding IEEE Conference on Decision and Control, Los Angeles, CA, 15–17 December 2014.

[24]

Schmerling E, Leung K, and Vollprecht W, et al. (2018) Multimodal probabilistic model-based planning for human-robot interaction. In: Proceeding IEEE Conference on Robotics and Automation, Brisbane, QLD, 21–25 May 2018.

[25]

Vazquez-Chanlatte M, Deshmukh JV, and Jin X, et al. (2017) Logical clustering and learning for time-series data. In: Proceeding International Conference Computer Aided Verification, Heidelberg, Germany, 24–28 July 2017 10426, pp. 305–325.

[26]

Wongpiromsarn T, Topcu U, and Ozay N, et al. (2011) TuLiP: A software toolbox for receding horizon temporal logic planning. In: Hybrid Systems: Computation and Control, Chicago, IL, 12–14 April 2011.

[27]

Yaghoubi S and Fainekos G (2019) Worst-case satisfaction of STL specifications using feedforward neural network controllers: A lagrange multipliers approach. ACM Transactions on Embedded Computing Systems 18(5s).

Digital Library

Cited By

Yu PGao YJiang FJohansson KDimarogonas D(2024)Online control synthesis for uncertain systems under signal temporal logic specificationsInternational Journal of Robotics Research10.1177/0278364923121257243:6(765-790)Online publication date: 1-May-2024
https://dl.acm.org/doi/10.1177/02783649231212572
Hashemi NHoxha BProkhorov DFainekos GDeshmukh J(2024)Scaling Learning-based Policy Optimization for Temporal Logic Tasks by Controller Network DropoutACM Transactions on Cyber-Physical Systems10.1145/36961128:4(1-28)Online publication date: 16-Sep-2024
https://dl.acm.org/doi/10.1145/3696112
Khandait TPedrielli G(2024)HyperPart-X: Probabilistic Guarantees for Parameter Mining of Signal Temporal Logic Formulas in Cyber-Physical SystemsRuntime Verification10.1007/978-3-031-74234-7_6(89-106)Online publication date: 14-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-74234-7_6
Show More Cited By

Recommendations

A program logic to verify signal temporal logic specifications of hybrid systems
HSCC '21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control

Signal temporal logic (STL) was introduced for monitoring temporal properties of continuous-time signals for continuous and hybrid systems. Differential dynamic logic (dL) was introduced to reason about the end states of a hybrid program. Over the past ...
Extending Signal Temporal Logic with Quantitative Semantics by Intervals for Robust Monitoring of Cyber-physical Systems
Special Issue on Time for CPS and Regular Papers

Monitoring is the core procedure of runtime verification of cyber-physical systems (CPS) and provides an evaluation of a signal with respect to a given specification. For formally specifying requirements with time constraints for CPS, Signal Temporal ...
Online control synthesis for uncertain systems under signal temporal logic specifications

Signal temporal logic (STL) formulas have been widely used as a formal language to express complex robotic specifications, thanks to their rich expressiveness and explicit time semantics. Existing approaches for STL control synthesis suffer from limited ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image International Journal of Robotics Research

International Journal of Robotics Research Volume 42, Issue 6

May 2023

160 pages

ISSN:0278-3649

Issue’s Table of Contents

© The Author(s) 2022.

Publisher

Sage Publications, Inc.

United States

Publication History

Published: 01 May 2023

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 20 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Yu PGao YJiang FJohansson KDimarogonas D(2024)Online control synthesis for uncertain systems under signal temporal logic specificationsInternational Journal of Robotics Research10.1177/0278364923121257243:6(765-790)Online publication date: 1-May-2024
https://dl.acm.org/doi/10.1177/02783649231212572
Hashemi NHoxha BProkhorov DFainekos GDeshmukh J(2024)Scaling Learning-based Policy Optimization for Temporal Logic Tasks by Controller Network DropoutACM Transactions on Cyber-Physical Systems10.1145/36961128:4(1-28)Online publication date: 16-Sep-2024
https://dl.acm.org/doi/10.1145/3696112
Khandait TPedrielli G(2024)HyperPart-X: Probabilistic Guarantees for Parameter Mining of Signal Temporal Logic Formulas in Cyber-Physical SystemsRuntime Verification10.1007/978-3-031-74234-7_6(89-106)Online publication date: 14-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-74234-7_6
Kudalkar VHashemi NMukhopadhyay SMallick SBudnik CNagaraja PDeshmukh J(2024)Sampling-Based and Gradient-Based Efficient Scenario GenerationRuntime Verification10.1007/978-3-031-74234-7_5(70-88)Online publication date: 14-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-74234-7_5
Baert MLeroux SSimoens P(2024)Learning Temporal Task Specifications From DemonstrationsExplainable and Transparent AI and Multi-Agent Systems10.1007/978-3-031-70074-3_5(81-98)Online publication date: 6-May-2024
https://dl.acm.org/doi/10.1007/978-3-031-70074-3_5

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents