EECI 2013: Synthesis of Reactive Control Protocols - Revision history

Murray: /* Further Reading */

2013-03-21T08:10:23Z

Further Reading

← Older revision		Revision as of 08:10, 21 March 2013
Line 9:		Line 9:

	== Further Reading ==		== Further Reading ==
	* <p>[http://portal.acm.org/citation.cfm?id=101990 On the development of reactive systems], D. Harel and A. Pnueli </p>		* <p>[http://portal.acm.org/citation.cfm?id=101990 On the development of reactive systems], D. Harel and A. Pnueli. In ''Logics and models of concurrent systems'', Pages 477 - 498, Springer-Verlag, 1985.</p>
	* <p>[http://ysaar.net/data/synth.pdf Synthesis of Reactive(1) Designs.], Nir Priterman, Amir Pnueli, and Yaniv Sa'ar. In Proc. 7th International Conference on Verification, Model Checking and Abstract Interpretation, volume 3855 of Lecture Notes in Computer Science, pages 364-380, 2006. Software available at http://jtlv.sourceforge.net/.</p>		* <p>[http://ysaar.net/data/synth.pdf Synthesis of Reactive(1) Designs.], Nir Priterman, Amir Pnueli, and Yaniv Sa'ar. In Proc. 7th International Conference on Verification, Model Checking and Abstract Interpretation, volume 3855 of Lecture Notes in Computer Science, pages 364-380, 2006. Software available at http://jtlv.sourceforge.net/.</p>

Murray: /* Further Reading */

2013-03-21T08:08:46Z

Further Reading

← Older revision		Revision as of 08:08, 21 March 2013
Line 10:		Line 10:
	== Further Reading ==		== Further Reading ==
	* <p>[http://portal.acm.org/citation.cfm?id=101990 On the development of reactive systems], D. Harel and A. Pnueli </p>		* <p>[http://portal.acm.org/citation.cfm?id=101990 On the development of reactive systems], D. Harel and A. Pnueli </p>
	* <p>[http://ysaar.net/data/synth.pdf Synthesis of Reactive(1) Designs.], Nir Priterman, Amir Pnueli, and Yaniv Sa'ar. In Proc. 7th International Conference on Verification, Model Checking and Abstract Interpretation, volume 3855 of Lecture Notes in Computer Science, pages 364-380, ~~2005~~. ~~software~~ available at http://jtlv.sourceforge.net/.</p>		* <p>[http://ysaar.net/data/synth.pdf Synthesis of Reactive(1) Designs.], Nir Priterman, Amir Pnueli, and Yaniv Sa'ar. In Proc. 7th International Conference on Verification, Model Checking and Abstract Interpretation, volume 3855 of Lecture Notes in Computer Science, pages 364-380, 2006. Software available at http://jtlv.sourceforge.net/.</p>

Murray: /* Further Reading */

2013-03-21T08:08:26Z

Further Reading

← Older revision		Revision as of 08:08, 21 March 2013
Line 10:		Line 10:
	== Further Reading ==		== Further Reading ==
	* <p>[http://portal.acm.org/citation.cfm?id=101990 On the development of reactive systems], D. Harel and A. Pnueli </p>		* <p>[http://portal.acm.org/citation.cfm?id=101990 On the development of reactive systems], D. Harel and A. Pnueli </p>
	* <p>[http://ysaar.net/data/synth.pdf Synthesis of Reactive(1) Designs.], Nir Priterman, Amir Pnueli, and Yaniv Sa'ar. In Proc. 7th International Conference on Verification, Model Checking and Abstract Interpretation, volume 3855 of Lecture Notes in Computer Science, pages 364-380, ~~2006~~.</p>		* <p>[http://ysaar.net/data/synth.pdf Synthesis of Reactive(1) Designs.], Nir Priterman, Amir Pnueli, and Yaniv Sa'ar. In Proc. 7th International Conference on Verification, Model Checking and Abstract Interpretation, volume 3855 of Lecture Notes in Computer Science, pages 364-380, 2005. software available at http://jtlv.sourceforge.net/.</p>

Murray: /* Further Reading */

2013-03-21T08:04:29Z

Further Reading

← Older revision		Revision as of 08:04, 21 March 2013
Line 10:		Line 10:
	== Further Reading ==		== Further Reading ==
	* <p>[http://portal.acm.org/citation.cfm?id=101990 On the development of reactive systems], D. Harel and A. Pnueli </p>		* <p>[http://portal.acm.org/citation.cfm?id=101990 On the development of reactive systems], D. Harel and A. Pnueli </p>
	* <p>[http://ysaar.net/data/synth.pdf Synthesis of Reactive(1) Designs.], Nir Priterman, Amir Pnueli, and Yaniv Sa'ar.		* <p>[http://ysaar.net/data/synth.pdf Synthesis of Reactive(1) Designs.], Nir Priterman, Amir Pnueli, and Yaniv Sa'ar. In Proc. 7th International Conference on Verification, Model Checking and Abstract Interpretation, volume 3855 of Lecture Notes in Computer Science, pages 364-380, 2006.</p>
	In Proc. 7th International Conference on Verification, Model Checking and Abstract Interpretation, volume 3855 of Lecture Notes in Computer Science, pages 364-380, 2006.</p>

Murray: /* Further Reading */

2013-03-21T08:04:04Z

Further Reading

← Older revision		Revision as of 08:04, 21 March 2013
Line 9:		Line 9:

	== Further Reading ==		== Further Reading ==
	* <p>[http://portal.acm.org/citation.cfm?id=101990 On the development of reactive systems], D. Harel and A. Pnueli,		* <p>[http://portal.acm.org/citation.cfm?id=101990 On the development of reactive systems], D. Harel and A. Pnueli </p>
	* <p>[http://ysaar.net/data/synth.pdf Synthesis of Reactive(1) Designs.], Nir Priterman, Amir Pnueli, and Yaniv Sa'ar.		* <p>[http://ysaar.net/data/synth.pdf Synthesis of Reactive(1) Designs.], Nir Priterman, Amir Pnueli, and Yaniv Sa'ar.
	In Proc. 7th International Conference on Verification, Model Checking and Abstract Interpretation, volume 3855 of Lecture Notes in Computer Science, pages 364-380, 2006.		In Proc. 7th International Conference on Verification, Model Checking and Abstract Interpretation, volume 3855 of Lecture Notes in Computer Science, pages 364-380, 2006.</p>

Murray: /* Further Reading */

2013-03-21T08:03:44Z

Further Reading

← Older revision		Revision as of 08:03, 21 March 2013
Line 10:		Line 10:
	== Further Reading ==		== Further Reading ==
	* <p>[http://portal.acm.org/citation.cfm?id=101990 On the development of reactive systems], D. Harel and A. Pnueli,		* <p>[http://portal.acm.org/citation.cfm?id=101990 On the development of reactive systems], D. Harel and A. Pnueli,
			* <p>[http://ysaar.net/data/synth.pdf Synthesis of Reactive(1) Designs.], Nir Priterman, Amir Pnueli, and Yaniv Sa'ar.
			In Proc. 7th International Conference on Verification, Model Checking and Abstract Interpretation, volume 3855 of Lecture Notes in Computer Science, pages 364-380, 2006.

Murray at 08:01, 21 March 2013

2013-03-21T08:01:01Z

← Older revision		Revision as of 08:01, 21 March 2013
Line 6:		Line 6:

	== Lecture Materials ==		== Lecture Materials ==
	* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-~~sp12~~/L7_reactive-20Mar13.pdf Synthesis of Reactive Control Protocols]		* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp13/L7_reactive-20Mar13.pdf Synthesis of Reactive Control Protocols]

	== Further Reading ==		== Further Reading ==
	* <p>[http://portal.acm.org/citation.cfm?id=101990 On the development of reactive systems], D. Harel and A. Pnueli,		* <p>[http://portal.acm.org/citation.cfm?id=101990 On the development of reactive systems], D. Harel and A. Pnueli,

Murray: /* Lecture Materials */

2013-03-21T08:00:16Z

Lecture Materials

← Older revision		Revision as of 08:00, 21 March 2013
Line 6:		Line 6:

	== Lecture Materials ==		== Lecture Materials ==
	* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/~~L7_reactive_synthesis~~-20Mar13.pdf Synthesis of Reactive Control Protocols]		* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/L7_reactive-20Mar13.pdf Synthesis of Reactive Control Protocols]

	== Further Reading ==		== Further Reading ==
	* <p>[http://portal.acm.org/citation.cfm?id=101990 On the development of reactive systems], D. Harel and A. Pnueli,		* <p>[http://portal.acm.org/citation.cfm?id=101990 On the development of reactive systems], D. Harel and A. Pnueli,

Murray: Created page with "{{eeci-sp13 header|prev= Algorithmic Verification|next=Computer Session: TuLiP}} This lecture discusses planner synthesis from LTL specification. In particular, we focus on s..."

2013-03-20T06:57:58Z

Created page with "{{eeci-sp13 header|prev= Algorithmic Verification|next=Computer Session: TuLiP}} This lecture discusses planner synthesis from LTL specification. In particular, we focus on s..."

New page

{{eeci-sp13 header|prev= Algorithmic Verification|next=Computer Session: TuLiP}}

This lecture discusses planner synthesis from LTL specification. In particular, we focus on systems that maintain an ongoing interaction with their environment. For the system to be correct, the planner needs to ensure that the specification holds for all the possible behaviors of the environment. This "reactive" system synthesis problem originates from Church's problem formulated in 1965 and can be viewed as a two-person game between the system and the environment. In general, the complexity of reactive system synthesis problem is double exponential. However, for certain special cases, the problem can be solved in polynomial time. We discuss those special cases, with the emphasis on the case where the problem can be formulated as a Generalized Reactivity(1) game.

{{righttoc}}

== Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/L7_reactive_synthesis-20Mar13.pdf Synthesis of Reactive Control Protocols]

== Further Reading ==
* <p>[http://portal.acm.org/citation.cfm?id=101990 On the development of reactive systems], D. Harel and A. Pnueli,