EECI 2012: Model Checking and Logic Synthesis - Revision history

Murray: /* Additional Information */

2012-05-14T09:38:51Z

Additional Information

← Older revision		Revision as of 09:38, 14 May 2012
Line 14:		Line 14:

	== Additional Information ==		== Additional Information ==
	* [http://spinroot.com/spin/whatispin.html Spin website]

Murray at 09:38, 14 May 2012

2012-05-14T09:38:32Z

← Older revision		Revision as of 09:38, 14 May 2012
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 [[EECI 2012: Computer Session: Spin\|~~Computer Session:~~ Spin]] lecture) and discuss the computational complexity of model checking.		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 ==

Murray at 09:38, 14 May 2012

2012-05-14T09:38:11Z

← Older revision		Revision as of 09:38, 14 May 2012
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 [[EECI 2012; Computer Session: Spin\|Computer Session: Spin]] lecture) and discuss the computational complexity of model checking.		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 [[EECI 2012: Computer Session: Spin\|Computer Session: Spin]] lecture) and discuss the computational complexity of model checking.

	== Lecture Materials ==		== Lecture Materials ==

Murray at 09:37, 14 May 2012

2012-05-14T09:37:54Z

← Older revision		Revision as of 09:37, 14 May 2012
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\|Computer Session: Spin]] lecture) and discuss the computational complexity of model checking.		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 [[EECI 2012; Computer Session: Spin\|Computer Session: Spin]] lecture) and discuss the computational complexity of model checking.

	== Lecture Materials ==		== Lecture Materials ==

Murray: /* Further Reading */

2012-05-14T09:25:56Z

Murray: /* Lecture Materials */

2012-05-14T09:17:15Z

Lecture Materials

← Older revision		Revision as of 09:17, 14 May 2012
Line 6:		Line 6:

	== Lecture Materials ==		== Lecture Materials ==
	* Lecture slides: [http://www.cds.caltech.edu/~murray/~~coures~~/eeci-sp12/L4_model_checking-14May12.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-sp12/L4_model_checking-14May12.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: /* Lecture Materials */

2012-05-14T09:13:00Z

Lecture Materials

← Older revision		Revision as of 09:13, 14 May 2012
Line 6:		Line 6:

	== Lecture Materials ==		== Lecture Materials ==
	* Lecture slides: [http://dl.~~dropbox~~.~~com~~/u/~~29005314~~/~~L4_Model_Checking_Logic_Synthesis~~-14May12.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/coures/eeci-sp12/L4_model_checking-14May12.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 19:18, 13 May 2012

2012-05-13T19:18:16Z

← Older revision		Revision as of 19:18, 13 May 2012
Line 1:		Line 1:
	{{~~AFRL12~~ header\|prev=Temporal Logic \|next=Computer Session: Spin}}		{{eeci-sp12 header\|prev=Temporal Logic \|next=Computer Session: Spin}}

	{{righttoc}}		{{righttoc}}

Tw68: /* Lecture Materials */

2012-05-10T03:59:31Z

Lecture Materials

← Older revision		Revision as of 03:59, 10 May 2012
Line 6:		Line 6:

	== Lecture Materials ==		== Lecture Materials ==
	* Lecture slides: [http://~~www~~.~~cds~~.~~caltech.edu~~/~~~utopcu~~/~~AFRL2012~~/L4_Model_Checking_Logic_Synthesis.pdf Model Checking and Logic Synthesis] (Presentation and notation follow that in "Model Checking" chapter 5.2 by Baier and Katoen.)		* Lecture slides: [http://dl.dropbox.com/u/29005314/L4_Model_Checking_Logic_Synthesis-14May12.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 ==

Utopcu: /* Further Reading */

2012-04-22T02:30:34Z

← Older revision		Revision as of 09:25, 14 May 2012
Line 9:		Line 9:

	== Further Reading ==		== Further Reading ==
	* <p>[http://www.amazon.com/SPIN-Model-Checker-Primer-Reference/dp/0321228626/ref=sr_1_1?ie=UTF8&qid=1297068669&sr=8-1 The SPIN Model Checker: Primer and Reference Manual], G. J. Holzmann, Addison-Wesley Professional, 2003. A comprehensive reference on Spin model checker </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://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>

← Older revision		Revision as of 02:30, 22 April 2012
Line 12:		Line 12:
	* <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>
			* <p>[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</p>

	== Additional Information ==		== Additional Information ==
	* [http://spinroot.com/spin/whatispin.html Spin website]		* [http://spinroot.com/spin/whatispin.html Spin website]