EECI 2012: Synthesis of Reactive Control Protocols - Revision history

Murray at 07:27, 17 May 2012

2012-05-17T07:27:44Z

← Older revision		Revision as of 07:27, 17 May 2012
Line 1:		Line 1:
	{{eeci-sp12 header\|prev= Algorithmic Verification\|next=Computer ~~Lab~~: TuLiP}}		{{eeci-sp12 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.		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.
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, ~~Logics and models of concurrent systems, Springer-Verlag New York, Inc., 1985, pp. 477–498. For discussion about closed and open systems</p>~~		* <p>[http://portal.acm.org/citation.cfm?id=101990 On the development of reactive systems], D. Harel and A. Pnueli,

	* <p>[http://www.mathunion.org/ICM/ICM1962.1/Main/icm1962.1.0023.0058.ocr.pdf Logic, arithmetics, and automata], A. Church, Proceedings of the international congress of mathematicians, 1962. An article on Church’s solvability problem [Thanks to Scott Livingston for pointing that all ICM proceedings (and this paper in particular) are available at this [http://www.mathunion.org/ICM/ link].] </p>

	* <p>[http://portal.acm.org/citation.cfm?id=75293 On the synthesis of a reactive module], A. Pnueli and R. Rosner, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 1989. A good reference on reactive module synthesis</p>

	* <p>[http://jtlv.ysaar.net/resources/publications/synth.pdf Synthesis of reactive(1) designs], N. Piterman, A. Pnueli and Y. Sa’ar, Verification, Model Checking and Abstract Interpretation, Springer, 2006. </p>

	~~== Additional Information ==~~
	* [http://jtlv.ysaar.net/ JTLV project] A Framework where GR(1) synthesis is implemented

Murray: /* Lecture Materials */

2012-05-17T07:26:35Z

Lecture Materials

← Older revision		Revision as of 07:26, 17 May 2012
Line 6:		Line 6:

	== Lecture Materials ==		== Lecture Materials ==
	* Lecture slides: [http://dl.~~dropbox~~.~~com~~/u/~~29005314~~/L7_reactive_synthesis-16May12.pdf Synthesis of Reactive Control Protocols]		* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/L7_reactive_synthesis-16May12.pdf Synthesis of Reactive Control Protocols]

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

Murray at 13:14, 16 May 2012

2012-05-16T13:14:49Z

← Older revision		Revision as of 13:14, 16 May 2012
Line 1:		Line 1:
	{{~~AFRL12~~ header\|prev=~~Computer Lab I~~ \|next=~~Receding Horizon Temporal Logic Planning~~}}		{{eeci-sp12 header\|prev= Algorithmic Verification\|next=Computer Lab: 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.		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.

Tw68: /* Lecture Materials */

2012-05-10T04:02:26Z

Lecture Materials

← Older revision		Revision as of 04:02, 10 May 2012
Line 6:		Line 6:

	== Lecture Materials ==		== Lecture Materials ==
	* Lecture slides: [http://~~www~~.~~cds~~.~~caltech.edu~~/~~~murray~~/~~courses/afrl-sp12~~/~~L7_reactive~~-~~25Apr12~~.pdf Synthesis of Reactive Control Protocols]		* Lecture slides: [http://dl.dropbox.com/u/29005314/L7_reactive_synthesis-16May12.pdf Synthesis of Reactive Control Protocols]

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

Murray: /* Lecture Materials */

2012-04-26T19:08:30Z

Lecture Materials

← Older revision		Revision as of 19:08, 26 April 2012
Line 6:		Line 6:

	== Lecture Materials ==		== Lecture Materials ==
	* Lecture slides: [http://www.cds.caltech.edu/~murray/afrl-sp12/L7_reactive-25Apr12.pdf Synthesis of Reactive Control Protocols]		* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/afrl-sp12/L7_reactive-25Apr12.pdf Synthesis of Reactive Control Protocols]

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

Murray: /* Lecture Materials */

2012-04-26T19:08:05Z

Lecture Materials

← Older revision		Revision as of 19:08, 26 April 2012
Line 6:		Line 6:

	== Lecture Materials ==		== Lecture Materials ==
	* Lecture slides: [http://www.cds.caltech.edu/~murray/afrl-sp12/L7_reactive-~~15Apr12~~.pdf Synthesis of Reactive Control Protocols]		* Lecture slides: [http://www.cds.caltech.edu/~murray/afrl-sp12/L7_reactive-25Apr12.pdf Synthesis of Reactive Control Protocols]

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

Murray: Created page with '{{AFRL12 header|prev=Computer Lab I |next=Receding Horizon Temporal Logic Planning}} This lecture discusses planner synthesis from LTL specification. In particular, we focus on …'

2012-04-25T18:31:33Z

Created page with '{{AFRL12 header|prev=Computer Lab I |next=Receding Horizon Temporal Logic Planning}} This lecture discusses planner synthesis from LTL specification. In particular, we focus on …'

New page

{{AFRL12 header|prev=Computer Lab I |next=Receding Horizon Temporal Logic Planning}}

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/afrl-sp12/L7_reactive-15Apr12.pdf Synthesis of Reactive Control Protocols]

== Further Reading ==
* [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

* [http://www.mathunion.org/ICM/ICM1962.1/Main/icm1962.1.0023.0058.ocr.pdf Logic, arithmetics, and automata], A. Church, Proceedings of the international congress of mathematicians, 1962. An article on Church’s solvability problem [Thanks to Scott Livingston for pointing that all ICM proceedings (and this paper in particular) are available at this [http://www.mathunion.org/ICM/ link].] 

* [http://portal.acm.org/citation.cfm?id=75293 On the synthesis of a reactive module], A. Pnueli and R. Rosner, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 1989. A good reference on reactive module synthesis

* [http://jtlv.ysaar.net/resources/publications/synth.pdf Synthesis of reactive(1) designs], N. Piterman, A. Pnueli and Y. Sa’ar, Verification, Model Checking and Abstract Interpretation, Springer, 2006. 

== Additional Information ==
* [http://jtlv.ysaar.net/ JTLV project] A Framework where GR(1) synthesis is implemented