# Difference between revisions of "EECI 2012: Synthesis of Reactive Control Protocols"

(3 intermediate revisions by 2 users not shown) | |||

Line 1: | Line 1: | ||

− | {{ | + | {{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 6: | Line 6: | ||

== Lecture Materials == | == Lecture Materials == | ||

− | * Lecture slides: [http://www.cds.caltech.edu/~murray/courses/ | + | * 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 == | ||

− | * <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, |

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− | |||

− |

## Latest revision as of 07:27, 17 May 2012

Prev: Algorithmic Verification | Course home | 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.

## Lecture Materials

- Lecture slides: Synthesis of Reactive Control Protocols

## Further Reading

On the development of reactive systems, D. Harel and A. Pnueli,