Literature

The topic of verification of hybrid systems is vast. While we only reserved a single week/chapter/block for it, it would easily fill a dedicated course, supported by a couple of books. Having a smaller time budget, we can still find some confirmation of usefulness even of a modest introduction in the Chapter 3 of [1]. Although we do not follow the book closely, we do cover some of their topics.

Among general references for hybrid system verification, we can recommend [2]. Although the book is not freely available for download, its web page contains quite some additional material such as slides and codes.

Reachability analysis

The overview paper [3] is recommendable. In addition, the manual for the CORA toolbox for Matlab [4] (by the same author and his team) can do a good tutorial job.

Barier certificates

We based our introduction on [5], including the example.

Temporal logics

Two popular monographs on model checking (based on temporal logics such as LTL, CTL and CTL*) are [6], and [7]. 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 [8], and [9].

A temporal logic particularly useful for specifying more complex requirements on (hybrid) control systems is STL. Its treatment of this framework in textbooks is still rather sketchy. Research papers are then the only source. STL has been introduced in [10]. Some more recent papers that also contain other relevant references are [11] and [12].

Back to top

References

[1]
H. Lin and P. J. Antsaklis, Hybrid Dynamical Systems: Fundamentals and Methods. in Advanced Textbooks in Control and Signal Processing. Cham: Springer, 2022. Accessed: Jul. 09, 2022. [Online]. Available: https://doi.org/10.1007/978-3-030-78731-8
[2]
S. Mitra, Verifying Cyber-Physical Systems: A Path to Safe Autonomy. in Cyber Physical Systems Series. Cambridge, MA, USA: MIT Press, 2021. Available: https://sayanmitracode.github.io/cpsbooksite/about.html
[3]
M. Althoff, G. Frehse, and A. Girard, “Set Propagation Techniques for Reachability Analysis,” Annual Review of Control, Robotics, and Autonomous Systems, vol. 4, no. 1, pp. 369–395, 2021, doi: 10.1146/annurev-control-071420-081941.
[4]
M. Althoff, N. Kochdumper, M. Wetzlinger, and T. Ladner, CORA 2024 Manual.” 2023. Accessed: Jan. 10, 2023. [Online]. Available: https://tumcps.github.io/CORA/data/archive/manual/Cora2024Manual.pdf
[5]
S. Prajna and A. Jadbabaie, “Safety Verification of Hybrid Systems Using Barrier Certificates,” in Hybrid Systems: Computation and Control, R. Alur and G. J. Pappas, Eds., in Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 2004, pp. 477–492. doi: 10.1007/978-3-540-24743-2_32.
[6]
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
[7]
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/
[8]
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
[9]
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
[10]
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.
[11]
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.
[12]
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.