EECI 2020: Model Checking - Revision history

Murray: /* Lecture Materials */

2020-03-10T07:56:30Z

Lecture Materials

← Older revision		Revision as of 07:56, 10 March 2020
Line 5:		Line 5:

	== Lecture Materials ==		== Lecture Materials ==
	* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp2020//L4_model_checking-~~10Mar2020~~.pdf Model Checking and Logic Synthesis] (Presentation and notation follow that in "Model Checking" chapter 5.2 by Baier and Katoen.)		* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp2020//L4_model_checking-09Mar2020.pdf Model Checking and Logic Synthesis] (Presentation and notation follow that in "Model Checking" chapter 5.2 by Baier and Katoen.)

	== Further Reading ==		== Further Reading ==

Murray at 07:47, 10 March 2020

2020-03-10T07:47:32Z

← Older revision		Revision as of 07:47, 10 March 2020
Line 5:		Line 5:

	== Lecture Materials ==		== Lecture Materials ==
	* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp2020//~~L4_model~~-~~checking-2020~~.pdf Model Checking and Logic Synthesis] (Presentation and notation follow that in "Model Checking" chapter 5.2 by Baier and Katoen.)		* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp2020//L4_model_checking-10Mar2020.pdf Model Checking and Logic Synthesis] (Presentation and notation follow that in "Model Checking" chapter 5.2 by Baier and Katoen.)

	== Further Reading ==		== Further Reading ==

Murray at 07:47, 10 March 2020

2020-03-10T07:47:08Z

← Older revision		Revision as of 07:47, 10 March 2020
Line 5:		Line 5:

	== Lecture Materials ==		== Lecture Materials ==
	* Lecture slides: [~~https~~://www.~~dropbox~~.~~com~~/s/~~lobibjtvnenmmz5~~/L4_model-checking-2020.pdf~~?dl=0~~ Model Checking and Logic Synthesis] (Presentation and notation follow that in "Model Checking" chapter 5.2 by Baier and Katoen.)		* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp2020//L4_model-checking-2020.pdf Model Checking and Logic Synthesis] (Presentation and notation follow that in "Model Checking" chapter 5.2 by Baier and Katoen.)

	== Further Reading ==		== Further Reading ==

Murray: /* Additional Information */

2020-02-29T23:18:58Z

Additional Information

← Older revision		Revision as of 23:18, 29 February 2020
Line 13:		Line 13:

	== Additional Information ==		== Additional Information ==
			* [http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/ LTL2BA] - a web page (and program) for converting LTL formulas to Buchi automata.

Murray at 16:56, 29 February 2020

2020-02-29T16:56:22Z

← Older revision		Revision as of 16:56, 29 February 2020
Line 1:		Line 1:
			{{eeci-sp2020 header\|prev=Temporal Logic\|next=Probabilistic Systems}}
	{{righttoc}}		{{righttoc}}

Nok: 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..."

2020-02-27T22:35:59Z

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

New page

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

== Lecture Materials ==
* Lecture slides: [https://www.dropbox.com/s/lobibjtvnenmmz5/L4_model-checking-2020.pdf?dl=0 Model Checking and Logic Synthesis] (Presentation and notation follow that in "Model Checking" chapter 5.2 by Baier and Katoen.)

== Further Reading ==
* [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. 
* [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. 
* [http://portal.acm.org/citation.cfm?id=101990 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 ==