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, i.e., 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 back-propagate through STL robustness formulas and hence enable a natural and easy-to-use integration with many gradient-based approaches used in robotics. We demonstrate, through examples stemming from various robotics applications, that stlcg is versatile, computationally efficient, and capable of injecting human-domain knowledge into the problem formulation.
K. Leung—This work was supported by the Office of Naval Research (Grant N00014- 17-1-2433) and by the Toyota Research Institute (“TRI”). This article solely reflects the opinions and conclusions of its authors and not of ONR, TRI or any other Toyota entity.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Equality and the other inequality relations can be derived from the STL grammar in (1), i.e., \(\mu (x) < c \Leftrightarrow -\mu (x) > -c\), and \(\mu (x) = c \Leftrightarrow \lnot (\mu (x) < c) \wedge \lnot (\mu (x) > c)\).
- 2.
This corresponds to padding the input trace with the last value of the robustness trace. A different value could be chosen instead. This applies to Cases 2–4 as well.
- 3.
We can even account for variable signal length by padding the inputs and keeping track of the signal lengths.
- 4.
The \(\epsilon _{ij}\)’s are initialized to zero, which gives negative robustness values and hence results in a non-zero gradient.
References
Bartocci, E., Deshmukh, J., Donzé, A., Fainekos, G., Maler, O., Nickovic, D., Sankaranarayanan, S.: Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In: Lectures on Runtime Verification, pp. 135–175 (2018)
Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Proceedings of International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, Formal Modeling and Analysis of Timed Systems (2004)
Pant, Y.V., Abbas, H., Mangharam, R.: Smooth operator: control using the smooth robustness of temporal logic. In: IEEE Conference on Control Technology and Applications (2017)
Li, X., Vasile, C.I., Belta, C.: Reinforcement learning with temporal logic rewards. In: IEEE/RSJ International Conference on Intelligent Robots and Systems (2017)
Raman, V., Donze, A., Maasoumy, M., Murray, R.M., Sangiovanni-Vincentelli, A., Seshia, S.A.: Model predictive control with signal temporal logic specifications. In: Proceedings of IEEE Conference on Decision and Control (2014)
Mehr, N., Sadigh, D., Horowitz, R., Sastry, S., Seshia, S.A.: Stochastic predictive freeway ramp metering from signal temporal logic specifications. In: American Control Conference (2017)
Sadigh, D., Kapoor, A.: Safe control under uncertainty with probabilistic signal temporal logic. In: Robotics: Science and Systems (2016)
Chinchali, S.P., Livingston, S.C., Chen, M., Pavone, M.: Multi-objective optimal control for proactive decision-making with temporal logic models. Int. J. Robot. Res. 38(12–13), 1490–1512 (2019)
Yaghoubi, S., Fainekos, G.: Worst-case satisfaction of STL specifications using feedforward neural network controllers: a lagrange multipliers approach. ACM Trans. Embed. Comput. Syst. 18(5s), 1–20 (2019)
Aksaray, D., Jones, A., Kong, Z., Schwager, M., Belta, C.: Q-learning for robust satisfaction of signal temporal logic specifications. In: Proceedings of IEEE Conference on Decision and Control (2014)
Li, X., Ma, Y., Belta, C.: A policy search method for temporal logic specified reinforcement learning tasks. In: American Control Conference (2018)
Vazquez-Chanlatte, M., Deshmukh, J.V., Jin, X., Seshia, S.A.: Logical clustering and learning for time-series data. In: Proceedings of International Conference on Computer Aided Verification, vol. 10426, pp. 305–325 (2017)
Asarin, E., Donzé, A., Maler, O., Nickovic, D.: Parametric identification of temporal properties. In: International Conference on Runtime Verification (2012)
Liu, C., Arnon, T., Lazarus, C., Barrett, C., Kochenderfer, M.J.: Algorithms for verifying deep neural networks (2019). https://arxiv.org/abs/1903.06758
Paszke, A., Gross, S., Chintala, S., Chanan, G., Yang, E., DeVito, Z., Lin, Z., Desmaison, A., Antiga, L., Lerer, A.: Automatic differentiation in PyTorch. In: Conference on Neural Information Processing Systems - Autodiff Workshop (2017)
Fainekos, G., Sankaranarayanan, S., Ueda, K., Yazarel, H.: Verification of automotive control applications using S-TaLiRo. In: American Control Conference (2012)
Hochreiter, S., Schmidhuber, J.: Long short-term memory. Neural Comput. 9(8), 1735–1780 (1997)
Mehdipour, N., Vasile, C.I., Belta, C.: Arithmetic-geometric mean robustness for control from signal temporal logic specifications. In: American Control Conference (2019)
Gers, F.A., Schmidhuber, J., Cummins, F.: Learning to forget: continual prediction with LSTM. In: International Conference on Artificial Neural Networks (1999)
Schmerling, E., Leung, K., Vollprecht, W., Pavone, M.: Multimodal probabilistic model-based planning for human-robot interaction. In: Proceedings of IEEE Conference on Robotics and Automation (2018)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Leung, K., Arechiga, N., Pavone, M. (2021). Back-Propagation Through Signal Temporal Logic Specifications: Infusing Logical Structure into Gradient-Based Methods. In: LaValle, S.M., Lin, M., Ojala, T., Shell, D., Yu, J. (eds) Algorithmic Foundations of Robotics XIV. WAFR 2020. Springer Proceedings in Advanced Robotics, vol 17. Springer, Cham. https://doi.org/10.1007/978-3-030-66723-8_26
Download citation
DOI: https://doi.org/10.1007/978-3-030-66723-8_26
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-66722-1
Online ISBN: 978-3-030-66723-8
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)