Difference between revisions of "EECI 2012: Model Checking and Logic Synthesis"
| (4 intermediate revisions by the same user not shown) | |||
| Line 3: | Line 3: | ||
{{righttoc}} | {{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 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 [[Computer Session: Spin| | 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 the [[EECI 2012: Computer Session: Spin|Spin]] lecture) and discuss the computational complexity of model checking. | ||
== Lecture Materials == | == Lecture Materials == | ||
| Line 9: | Line 9: | ||
== Further Reading == | == Further Reading == | ||
* <p>[http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=11481 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. </p> | * <p>[http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=11481 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. </p> | ||
* <p>[http://www.amazon.com/Model-Checking-Edmund-Clarke-Jr/dp/0262032708/ref=sr_1_1?s=books&ie=UTF8&qid=1297071898&sr=1-1 Model Checking], E. M. Clarke, O. Grumberg and D. A. Peled, The MIT Press, 1999. A very good reference on automata based model checking. </p> | * <p>[http://www.amazon.com/Model-Checking-Edmund-Clarke-Jr/dp/0262032708/ref=sr_1_1?s=books&ie=UTF8&qid=1297071898&sr=1-1 Model Checking], E. M. Clarke, O. Grumberg and D. A. Peled, The MIT Press, 1999. A very good reference on automata based model checking. </p> | ||
| Line 15: | Line 14: | ||
== Additional Information == | == Additional Information == | ||
Latest revision as of 09:38, 14 May 2012
| Prev: Temporal Logic | Course home | Next: Computer Session: Spin |
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 the Spin lecture) and discuss the computational complexity of model checking.
Lecture Materials
- Lecture slides: Model Checking and Logic Synthesis (Presentation and notation follow that in "Model Checking" chapter 5.2 by Baier and Katoen.)
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
