Murray Wiki - User contributions [en]

EECI 2012: Computer Session: TuLiP

2012-05-10T04:49:57Z

Tw68: /* Lecture Materials */

{{AFRL12 header|prev=Receding Horizon Temporal Logic Planning |next=....}}

This lecture provides an overview of TuLiP, a Python-based software toolbox for the synthesis of embedded control software that is provably correct with respect to a GR[1] specifications. TuLiP combines routines for (1) finite state abstraction of control systems, (2) digital design synthesis from GR[1] specifications, and (3) receding horizon planning. The underlying digital design synthesis routine treats the environment as adversary; hence, the resulting controller is guaranteed to be correct for any admissible environment profile. TuLiP applies the receding horizon framework, allowing the synthesis problem to be broken into a set of smaller problems, and consequently alleviating the computational complexity of the synthesis procedure, while preserving the correctness guarantee.

A brief overview of TuLiP will be followed by hands-on exercises using the toolbox.

== Lecture Materials ==
* Lecture slides: [http://dl.dropbox.com/u/29005314/C2_tulip-17May12.pdf TuLiP] (Exercises are at the end of the slides.)
* MATLAB plotting: [http://dl.dropbox.com/u/29005314/plotRobotSim.m plotRobotSim.m], [http://dl.dropbox.com/u/29005314/plotCarSim.m plotCarSim.m]
* [http://dl.dropbox.com/u/29005314/tulip_examples.zip Example TuLiP files] (zip file):
** 6 cell robot, discrete state space: [http://dl.dropbox.com/u/29005314/robot_discrete_simple.py robot_discrete_simple.py]
** 6 cell robot, with dynamics: [http://dl.dropbox.com/u/29005314/robot_simple.py robot_simple.py], [http://dl.dropbox.com/u/29005314/robot_simple2.py robot_simple2.py] (alternative formulation)

== Further Reading ==

* TuLiP: A Software Toolbox for Receding Horizon Temporal Logic Planning, T. Wongpiromsarn, U. Topcu, N. Ozay, H. Xu and R. M. Murray, Hybrid Systems: Computation and Control, 2011. 

== Additional Information ==
* [http://sourceforge.net/apps/mediawiki/tulip-control/index.php?title=Main_Page TuLiP on SourceForge] 
* [http://tulip-control.sourceforge.net/doc/ TuLiP Documentation] and [http://tulip-control.sourceforge.net/doc/install.html Installation instructions] 
* [http://jtlv.ysaar.net/ JTLV Project Home Site] JTLV provides the framework for the underlying digital design synthesis routine used in TuLiP.

EECI 2012: Synthesis of Reactive Control Protocols

2012-05-10T04:02:26Z

Tw68: /* Lecture Materials */

{{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://dl.dropbox.com/u/29005314/L7_reactive_synthesis-16May12.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

EECI 2012: Model Checking and Logic Synthesis

2012-05-10T03:59:31Z

Tw68: /* Lecture Materials */

{{AFRL12 header|prev=Temporal Logic |next=Computer Session: Spin}}

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

== 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.)

== Further Reading ==
* [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 
* [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 ==
* [http://spinroot.com/spin/whatispin.html Spin website]

EECI 2012: Automata Theory

2012-05-10T03:55:23Z

Tw68:

{{AFRL12 header|prev=Introduction |next=Temporal Logic}}

This lecture gives an introduction to some concepts and tools in computer science that are used in the remainder of the course. We start with finite transition systems as a mathematical model to describe behavior of systems with finite, discrete states. We use linear-time properties serve as the specification language (e.g., to specify safety or liveness properties) and we discuss the preliminaries that lead to model checking, a commonly used, powerful verification tool.

{{righttoc}}

== Lecture Materials ==
* Lecture slides: [http://dl.dropbox.com/u/29005314/L2_automata-theory-14May12.pdf Automata Theory] (presentation and notation follow that in "Principles of Model Checking" chapters 2.1, 2.2, 3.2-3.4 by Baier and Katoen.)

== Further Reading and Additional Information==
* [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. Early chapters provide an exposition to automata theory. Slides for this lecture follow this reference. 
* [http://www.amazon.com/Introduction-Theory-Computation-Michael-Sipser/dp/053494728X Introduction to the Theory of Computation], M. Sipser, PWS Publishing Company, 1997. This is a textbook on theory of computation covering preliminaries in automata theory. 
* [http://www.cds.caltech.edu/~utopcu/VerInCtrl/VerInCtrl.html CDS 270: Verification in Controls]: The second half of the course taught in Fall 2009 at Caltech also covered the material in this lecture. There are brief lecture notes and exercises.

EECI 2012: Automata Theory

2012-05-09T07:57:53Z

Tw68:

{{AFRL12 header|prev=Introduction |next=Temporal Logic}}

This lecture gives an introduction to some concepts and tools in computer science that are used in the remainder of the course. We start with finite transition systems as a mathematical model to describe behavior of systems with finite, discrete states. We use linear-time properties serve as the specification language (e.g., to specify safety or liveness properties) and we discuss the preliminaries that lead to model checking, a commonly used, powerful verification tool.

{{righttoc}}

== Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/AFRL2012/L2_Automata_Theory.pdf Automata Theory] (presentation and notation follow that in "Principles of Model Checking" chapters 2.1, 2.2, 3.2-3.4 by Baier and Katoen.)

== Further Reading and Additional Information==
* [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. Early chapters provide an exposition to automata theory. Slides for this lecture follow this reference. 
* [http://www.amazon.com/Introduction-Theory-Computation-Michael-Sipser/dp/053494728X Introduction to the Theory of Computation], M. Sipser, PWS Publishing Company, 1997. This is a textbook on theory of computation covering preliminaries in automata theory. 
* [http://www.cds.caltech.edu/~utopcu/VerInCtrl/VerInCtrl.html CDS 270: Verification in Controls]: The second half of the course taught in Fall 2009 at Caltech also covered the material in this lecture. There are brief lecture notes and exercises.