EECI 2020: Model Checking

From Murray Wiki
Revision as of 22:35, 27 February 2020 by Nok (talk | contribs) (Created page with "{{righttoc}} This lecture provides an introduction to automata based model checking and its use for closed system synthesis. We first discuss what model checking is, how it w...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

This lecture provides an introduction to automata based model checking and its use for closed system synthesis. We first discuss what model checking is, how it works (in particular how automata based model checking works), and how it is used for verification of linear temporal logic specifications against finite transition system models. We then move to its use for synthesizing (open-loop) control strategies.

Lecture Materials

Further Reading

  • Principles of Model Checking, C. Baier and J.-P. Katoen, The MIT Press, 2008. A detailed reference on model checking. Slides for this lecture follow Chapter 6 of this reference.

  • Model Checking, E. M. Clarke, O. Grumberg and D. A. Peled, The MIT Press, 1999. A very good reference on automata based model checking.

  • On the development of reactive systems, D. Harel and A. Pnueli, Logics and models of concurrent systems, Springer-Verlag New York, Inc., 1985, pp. 477–498. For discussion about closed and open systems

Additional Information