Literature

Two popular monographs on verification (model checking) based on temporal logics such as LTL, CTL and CTL* are [1], and [2]. These do not cover hybrid systems, though. Still they are recommendable (at least their first chapters) for understanding the basics.

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].

A temporal logic particularly useful for specifying more complex requirements on (hybrid) control systems is Signal Temporal Logic (STL). Its treatment of this framework in textbooks is still rather sketchy. Research papers are then the only source. STL has been introduced in the readable [5]. Robustness degree has been described in [6] and the self-contained slides [7]. Some more recent papers that also contain other relevant references are [8], [9], [10], [11].

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]
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.
[6]
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.
[7]
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
[8]
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.
[9]
V. Raman, M. Maasoumy, and A. Donzé, “Model predictive control from signal temporal logic specifications: A case study,” in Proceedings of the 4th ACM SIGBED International Workshop on Design, Modeling, and Evaluation of Cyber-Physical Systems, in CyPhy ’14. New York, NY, USA: Association for Computing Machinery, Apr. 2014, pp. 52–55. doi: 10.1145/2593458.2593472.
[10]
S. S. Farahani, V. Raman, and R. M. Murray, “Robust Model Predictive Control for Signal Temporal Logic Synthesis,” IFAC-PapersOnLine, vol. 48, no. 27, pp. 323–328, Jan. 2015, doi: 10.1016/j.ifacol.2015.11.195.
[11]
S. S. Farahani, R. Majumdar, V. S. Prabhu, and S. Soudjani, “Shrinking Horizon Model Predictive Control With Signal Temporal Logic Constraints Under Stochastic Disturbances,” IEEE Transactions on Automatic Control, vol. 64, no. 8, pp. 3324–3331, Aug. 2019, doi: 10.1109/TAC.2018.2880651.