Difference between revisions of "EECI 2012: Model Checking and Logic Synthesis"

From Murray Wiki
Jump to navigationJump to search
Line 1: Line 1:
{{AFRL12 header|prev=Temporal Logic |next=Computer Session: Spin}}

Revision as of 00:38, 22 April 2012

Return to Caltech/AFRL 2012 Main Page

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. We also provide examples using the SPIN model checker (discussed in XXX) and discuss the computational complexity of model checking.

Lecture Materials

Further Reading

  • The SPIN Model Checker: Primer and Reference Manual, G. J. Holzmann, Addison-Wesley Professional, 2003. A comprehensive reference on Spin model checker

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

Additional Information