Literature

Two popular monographs on formal verification (namely, model checking) based on temporal logics such as LTL, CTL and CTL* are [1], and [2]. These do not cover hybrid systems, but still reading at least their first chapters may help understand he fundamentals in this area.

Some learning material and sketches of applications of temporal logics in control systems for robotics and autonomous driving are in the lectures [3], and [4].

As we argued in the lecture, a temporal logic particularly useful for specifying more complex requirements on hybrid control systems is Signal Temporal Logic (STL). Treatment of this framework in textbooks is still rather sketchy (a very recent exception is [5]). Research papers are then the main learning resource. STL has been introduced in the readable [6]. Robustness degree has been described in [7] and the self-contained slides [8].

A selection of some more recent papers on STL that also contain other relevant references is: [9], [10], [11]. Clearly, research in this area is very active.

Back to top

References

[1]
C. Baier and J.-P. Katoen, Principles of Model Checking. Cambridge, MA, USA: MIT Press, 2008. Available: https://mitpress.mit.edu/books/principles-model-checking
[2]
E. M. Clarke, Jr, O. Grumberg, D. Kroening, D. Peled, and H. Veith, Model Checking, 2nd ed. in Cyber Physical Systems Series. Cambridge, MA, USA: MIT Press, 2018. Available: https://mitpress.mit.edu/9780262038836/model-checking/
[3]
R. M. Murray, U. Topcu, and N. Wongpiromsarn, “Lecture 3 Linear Temporal Logic (LTL).” Belgrade (Serbia), Mar. 2020. Available: http://www.cds.caltech.edu/~murray/courses/eeci-sp2020/L3_ltl-09Mar2020.pdf
[4]
N. Wongpiromsarn, R. M. Murray, and U. Topcu, “Lecture 4 Model Checking and Logic Synthesis.” Belgrade (Serbia), Mar. 2020. Available: http://www.cds.caltech.edu/~murray/courses/eeci-sp2020//L4_model_checking-09Mar2020.pdf
[5]
L. Lindemann and D. V. Dimarogonas, Formal Methods for Multi-Agent Feedback Control Systems. in Cyber-Physical Systems Series. The MIT Press, 2025. doi: 10.7551/mitpress/15136.001.0001.
[6]
O. Maler and D. Nickovic, “Monitoring Temporal Properties of Continuous Signals,” in Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Y. Lakhnech and S. Yovine, Eds., Berlin, Heidelberg: Springer, 2004, pp. 152–166. doi: 10.1007/978-3-540-30206-3_12.
[7]
A. Donzé and O. Maler, “Robust Satisfaction of Temporal Logic over Real-Valued Signals,” in Formal Modeling and Analysis of Timed Systems, K. Chatterjee and T. A. Henzinger, Eds., Berlin, Heidelberg: Springer, 2010, pp. 92–106. doi: 10.1007/978-3-642-15297-9_9.
[8]
A. Donzé, “On Signal Temporal Logic.” University of California, Berkeley, Feb. 2014. Available: https://people.eecs.berkeley.edu/~sseshia/fmee/lectures/EECS294-98_Spring2014_STL_Lecture.pdf
[9]
P. Yu, Y. Gao, F. J. Jiang, K. H. Johansson, and D. V. Dimarogonas, “Online control synthesis for uncertain systems under signal temporal logic specifications,” The International Journal of Robotics Research, vol. 43, no. 6, pp. 765–790, May 2024, doi: 10.1177/02783649231212572.
[10]
T. Yang, Y. Zou, S. Li, X. Yin, and T. Jia, “Signal temporal logic synthesis under Model Predictive Control: A low complexity approach,” Control Engineering Practice, vol. 143, p. 105782, Feb. 2024, doi: 10.1016/j.conengprac.2023.105782.
[11]
M. Charitidou and D. V. Dimarogonas, “Receding Horizon Control With Online Barrier Function Design Under Signal Temporal Logic Specifications,” IEEE Transactions on Automatic Control, vol. 68, no. 6, pp. 3545–3556, Jun. 2023, doi: 10.1109/TAC.2022.3195470.