Murray Wiki - User contributions [en]

EECI 2013: Computer Session: TuLiP

2013-03-20T19:59:18Z

Utopcu: /* Lecture Materials */

{{eeci-sp12 header|prev=RHTLP|next=Advanced Topcis}}

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://www.cds.caltech.edu/~utopcu/eeci13/C2_TuLiP-2013.pdf TuLiP]
* MATLAB plotting: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/plotRobotSim.m plotRobotSim.m], [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/plotCarSim.m plotCarSim.m]
* [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/tulip_examples.zip Example TuLiP files] (zip file):
** 6 cell robot, discrete state space: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/robot_discrete_simple.py robot_discrete_simple.py]
** 6 cell robot, with dynamics: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/robot_simple.py robot_simple.py], [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/robot_simple2.py robot_simple2.py] (alternative formulation)

== Further Reading ==

* [http://www.cds.caltech.edu/~murray/papers/2010n_wtoxm11-hscc.html 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 2013: Computer Session: TuLiP

2013-03-20T19:59:04Z

Utopcu:

{{eeci-sp12 header|prev=RHTLP|next=Advanced Topcis}}

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://www.cds.caltech.edu/~utopcu/eeci13/C2_TuLiP-2013.pdf TuLiP] (Exercises are at the end of the slides.)
* MATLAB plotting: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/plotRobotSim.m plotRobotSim.m], [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/plotCarSim.m plotCarSim.m]
* [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/tulip_examples.zip Example TuLiP files] (zip file):
** 6 cell robot, discrete state space: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/robot_discrete_simple.py robot_discrete_simple.py]
** 6 cell robot, with dynamics: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/robot_simple.py robot_simple.py], [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/robot_simple2.py robot_simple2.py] (alternative formulation)

== Further Reading ==

* [http://www.cds.caltech.edu/~murray/papers/2010n_wtoxm11-hscc.html 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 2013: Computer Session: TuLiP

2013-03-20T19:58:20Z

Utopcu:

{{eeci-sp12 header|prev=RHTLP|next=Advanced Topcis}}

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://www.cds.caltech.edu/~murray/courses/eeci-sp12/C2_tulip-17May12.pdf TuLiP] (Exercises are at the end of the slides.)
* MATLAB plotting: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/plotRobotSim.m plotRobotSim.m], [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/plotCarSim.m plotCarSim.m]
* [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/tulip_examples.zip Example TuLiP files] (zip file):
** 6 cell robot, discrete state space: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/robot_discrete_simple.py robot_discrete_simple.py]
** 6 cell robot, with dynamics: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/robot_simple.py robot_simple.py], [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/robot_simple2.py robot_simple2.py] (alternative formulation)

== Further Reading ==

* [http://www.cds.caltech.edu/~murray/papers/2010n_wtoxm11-hscc.html 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 2013: Computer Session: TuLiP

2013-03-20T19:57:38Z

Utopcu: Created page with "{{eeci-sp12 header|prev=Protocol Synthesis|next=RHTLP}} This lecture provides an overview of TuLiP, a Python-based software toolbox for the synthesis of embedded control soft..."

{{eeci-sp12 header|prev=Protocol Synthesis|next=RHTLP}}

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://www.cds.caltech.edu/~murray/courses/eeci-sp12/C2_tulip-17May12.pdf TuLiP] (Exercises are at the end of the slides.)
* MATLAB plotting: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/plotRobotSim.m plotRobotSim.m], [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/plotCarSim.m plotCarSim.m]
* [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/tulip_examples.zip Example TuLiP files] (zip file):
** 6 cell robot, discrete state space: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/robot_discrete_simple.py robot_discrete_simple.py]
** 6 cell robot, with dynamics: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/robot_simple.py robot_simple.py], [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/robot_simple2.py robot_simple2.py] (alternative formulation)

== Further Reading ==

* [http://www.cds.caltech.edu/~murray/papers/2010n_wtoxm11-hscc.html 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 2013: Algorithmic Verification of Hybrid Systems

2013-03-20T19:54:34Z

Utopcu: /* Further Reading */

{{eeci-sp13 header|prev=Deductive Verification|next=Protocol Synthesis}}

This lecture focuses on the verification of hybrid systems. We first discuss finite-state under- and over-approximations of hybrid dynamics and how these finite-state models coupled with the model checking tools can be used to verify temporal logic properties against hybrid dynamics. Then, we present a procedure for constructing finite-state, under-approximations which will later be used in the course in the synthesis of hierarchical control protocols. We finally introduce the notions of approximate bisimulations and bisimulation functions and how they can be used in verification of temporal properties.

== Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/eeci13/L6_Abstractions-2013.pdf Abstractions for the Analysis and Synthesis of Control Protocols for Hybrid Systems]

== Further Reading ==
* [http://robotics.eecs.berkeley.edu/~sastry/ee291e/lygeros.pdf Lecture Notes on Hybrid Systems] (by John Lygeros): A rough introduction to hybrid systems. Chapters 5 and 6 are on various analysis techniques relevant for this short course. 
* [http://www.cds.caltech.edu/~utopcu/images//4/4d/WTM-itac10R.pdf Receding horizon temporal logic planning],T. Wongpiromsarn, U. Topcu, and R. Murray, submitted to IEEE Transactions on Automatic Control, 2010. Details on the receding horizon temporal logic planning. 
* [http://www.cds.caltech.edu/~murray/wiki/index.php/EECI08:_Optimization-Based_Control Optimization based control]. A page prepared for EECI 2008 with information and material on basic receding horizon control.
* [http://control.ee.ethz.ch/~mpt/ Multiparametric Toolbox] The Multi-Parametric Toolbox (MPT) is a free Matlab toolbox for design, analysis and deployment of optimal controllers for constrained linear, nonlinear and hybrid systems. [http://www.cds.caltech.edu/tulip The receding horizon temporal logic planning toolbox] uses the polytope manipulation (intersection, union, set difference, projection, etc.) functionalities of MPT. 
* [http://www.cds.caltech.edu/~utopcu/images//9/98/WTM-aaai10.pdf Automatic synthesis of robust embedded control software], T. Wongpiromsarn, U. Topcu, and R. Murray, AAAI 2010 Spring Symposium on Embedded Reasoning: Intelligence in Embedded Systems, 2010. Details on the abstraction procedure covered in this lecture. 
* [http://www.mpc.berkeley.edu/mpc-course-material/BBMbook_Cambridge.pdf?attredirects=0&d=1 Predictive Control]: A book draft by Bemporap, Borrelli, and Morari. Details on some of the ideas in the implementation of the abstraction procedure presented in the slides can be found in this book. 
* [http://www.mpc.berkeley.edu/mpc-course-material/BBMbook_Cambridge.pdf?attredirects=0&d=1 Predictive Control]: A book draft by Bemporap, Borrelli, and Morari. Details on some of the ideas in the implementation of the abstraction procedure presented in the slides can be found in this book. 
* [http://www.cds.caltech.edu/~utopcu/eeci13/ltom-12-cdc.pdf Reactive controllers for differentially flat systems with temporal logic constraints], J. Liu, N. Ozay, U. Topcu, and R. Murray, Control and Decision Conference, 2012.

EECI 2013: Receding Horizon Temporal Logic Planning

2013-03-16T09:24:16Z

Utopcu:

{{eeci-sp13 header|prev=Synthesis of Reactive Control Protocols|next=Computer Session: TuliP}}

The first part of this lecture introduces the receding horizon temporal logic planning. Introductory material on high computational complexity of reactive control protocol synthesis is followed by the statement and discussion of a main result and a small example. We discuss implementation details, further extensions, and a hierarchical control structure that utilizes the proposed receding horizon temporal logic planning procedure.

== Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/eeci13/L8_RHTLP-2013.pdf Receding Horizon Temporal Logic Planning and Compositional Synthesis]

== Further Reading and Additional Information ==
* [http://www.cds.caltech.edu/~utopcu/images//4/4d/WTM-itac10R.pdf Receding horizon temporal logic planning],T. Wongpiromsarn, U. Topcu, and R. Murray, submitted to IEEE Transactions on Automatic Control, 2012. Details on the receding horizon temporal logic planning.

EECI 2013: Receding Horizon Temporal Logic Planning

2013-03-16T09:23:38Z

Utopcu:

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

The first part of this lecture introduces the receding horizon temporal logic planning. Introductory material on high computational complexity of reactive control protocol synthesis is followed by the statement and discussion of a main result and a small example. We discuss implementation details, further extensions, and a hierarchical control structure that utilizes the proposed receding horizon temporal logic planning procedure.

== Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/eeci13/L8_RHTLP-2013.pdf Receding Horizon Temporal Logic Planning and Compositional Synthesis]

== Further Reading and Additional Information ==
* [http://www.cds.caltech.edu/~utopcu/images//4/4d/WTM-itac10R.pdf Receding horizon temporal logic planning],T. Wongpiromsarn, U. Topcu, and R. Murray, submitted to IEEE Transactions on Automatic Control, 2012. Details on the receding horizon temporal logic planning.

EECI 2013: Receding Horizon Temporal Logic Planning

2013-03-16T09:23:16Z

Utopcu: Created page with "{{eeci-sp13 header|prev=Computer Session: TuLiP|next=Computer Session}} The first part of this lecture introduces the receding horizon temporal logic planning. Introductory m..."

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

The first part of this lecture introduces the receding horizon temporal logic planning. Introductory material on high computational complexity of reactive control protocol synthesis is followed by the statement and discussion of a main result and a small example. We discuss implementation details, further extensions, and a hierarchical control structure that utilizes the proposed receding horizon temporal logic planning procedure.

== Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/eeci13/L8_RHTLP-2013.pdf Receding Horizon Temporal Logic Planning and Compositional Synthesis]

== Further Reading and Additional Information ==
* [http://www.cds.caltech.edu/~utopcu/images//4/4d/WTM-itac10R.pdf Receding horizon temporal logic planning],T. Wongpiromsarn, U. Topcu, and R. Murray, submitted to IEEE Transactions on Automatic Control, 2012. Details on the receding horizon temporal logic planning.

HYCON-EECI, Spring 2013

2013-03-16T09:19:38Z

Utopcu: /* Lecture Schedule */

<table width="100%" cellspacing=0>
<tr valign=top>
<td rowspan=4 align=center> [[Image:eecilogo.png|90px]]</td>
<td align=center>Specification, Design, and Verification  </td>
<td rowspan=4 align=center"> [[Image:cdslogo.png|90px]]</td></tr>
<tr><td align=center>of Networked Control Systems   </td></tr>
<tr valign=top><td align=center> Richard M. Murray, Ufuk Topcu, and Nok Wongpiromsarn </td></tr>
<tr valign=top><td align=center>18-22 May 2013, Belgrade (Serbia)</td></tr>
</table> __NOTOC__

== Course Description ==
Increases in fast and inexpensive computing and communications have enabled a new generation of information-rich control systems that rely on multi-threaded networked execution, distributed optimization, sensor fusion and protocol stacks in increasingly sophisticated ways. This course will provide working knowledge of a collection of methods and tools for specifying, designing and verifying networked control systems. We combine methods from computer science (temporal logic, model checking, synthesis of control protocols) with those from dynamical systems and control (Lyapunov functions, trajectory generation, receding horizon control) to analyze and design partially asynchronous control protocols for continuous systems. In addition to introducing the mathematical techniques required to formulate problems and prove properties, we also describe a software toolbox (TuLiP) that is designed for analyzing and synthesizing hybrid control systems using linear temporal logic and robust performance specifications.

== Reading ==
The following papers and textbooks will be used heavily throughout the course:
* [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. 
* [http://www.cds.caltech.edu/~murray/papers/2012z_wtm12-us.html Synthesis of Control Protocols for Autonomous Systems], N. Wongpiromsarn, U. Topcu and R. M. Murray. ''Unmanned Systems'', 2013 (submitted)
Additional references for individual topics are included on the individual lecture pages.

== Course information ==
* Instructors: [http://www.cds.caltech.edu/~murray/wiki/Main_Page Richard M. Murray] (Caltech, CDS) and [http://www.cds.caltech.edu/~utopcu/index.php/Main_Page Ufuk Topcu] (Caltech, CDS), and [http://www.cds.caltech.edu/~nok/ Nok Wongpiromsarn] (MIT-Singapore)
* Date and location: 18-22 May 2013, Belgrade (Serbia)
* Sponsor: [http://www.eeci-institute.eu/GSC2013 HYCON-EECI Graduate School on Control]

== Lecture Schedule ==

The schedule below lists the lectures that will be given as part of the course. Each lecture will last approximately 90 minutes. The individual lecture pages give an overview of the lecture and links to additional information.

{|border=1 cellpadding=2
|-
|align=center|Lec
|align=center|Date/time
|Title
|Topics
{{eeci13 entry|L1|RM|Mon, 9:00|Introduction: Protocol-Based Control Systems|
* Introduction to networked control systems (NCS)
* Overview of control "protocols"
* Examples: Alice, RoboFlag
}}
{{eeci13 entry|L2|UT|Mon, 11:00|Automata Theory|
* Finite transition systems
* Paths, traces and composition of finite transition systems
* Linear time properties; safety and liveness
* Examples: traffic light
}}
{{eeci13 entry|L3|RM|Mon, 14:00|Temporal Logic|
* Linear temporal logic
* Omega regular properties
* Buchi automata, representation of LTL using NBA
* Examples: traffic light, (RoboFlag), autonomous driving
}}
{{eeci13 entry|L4|UT|Mon, 16:00|Model Checking and Logic Synthesis|
* Basic concepts in model checking
* Use of model checking for logic synthesis
* Examples: traffic light, farmer puzzle
}}
{{eeci13 entry|C1|RM|Tue, 9:00 Tue, 11:00|Computer Session: Spin|
* Introduction to Promela and Spin (statements, processes, messages)
* Verification examples: traffic light, distributed traffic light, gcdrive
* Synthesis examples: traffic light, farmer puzzle, robot navigation
}}
{{eeci13 entry|L5|RM (1h)|Wed, 9:00|Deductive Verification of Hybrid Systems|
* Brief introduction to hybrid systems and verification techniques (deductive, algorithmic)
* Deductive verification using barrier certificates
* Guarded command languages and CCL for asynchronous control protocols
* Examples: multi-agent systems, RoboFlag
}}
{{eeci13 entry|L6|UT (2h)|Wed, 11:00|Algorithmic Verification of Hybrid Systems|
* Abstraction hierarchies for control systems
* Finite state abstractions (discretization) and model checking
* Discretization of continuous state systems
* Approximate bi-simulation (if time)
* Examples: gear changing (?), ???
}}
{{eeci13 entry|L7|RM (2h)|Wed, 14:00|Synthesis of Reactive Control Protocols|
* Open system and reactive system synthesis
* Satisfiability, realizability
* Game structures, reachability/safety games
* Mu-calculus (if time) and GR(1) games
* Examples: runner-blocker
}}
{{eeci13 entry|L8|UT(1h)|Wed, 16:00|Receding Horizon Temporal Logic Planning|
* Receding horizon control
* Examples: reactive motion planning
}}
{{eeci13 entry|C2|UT|Thu, 9:00 Thu, 11:00|Computer Session: TuLiP|
* Introduction to TuLiP
* Synthesis of protocols for discrete systems
* Discretization of continuous systems (and protocol synthesis)
* Examples: reactive motion planning
}}
{{eeci13 entry|L9|UT|Fri, 9:00|Advanced Topics in Protocol Synthesis|
* Distributed control
* Switching
* Examples: reactive motion planning, electric power systems (distributed)
}}
{{eeci13 entry|L10|RM|Fri, 11:00|Extensions, Applications, Open Questions|
* Review of control trends and course contents
* Discussion of open problem areas and preliminary results
** Optimization-based techniques
** Probabilistic techniques
** Others: Robustness, switching systems, timed systems
* Examples: robot motion planning, electric power systems (timed)
}}
|}

== Software Installation ==

We will make use of two programs during the lab sessions:
* [http://spinroot.com Spin] - model checker for formal verification of distributed systems
* [http://tulip-control.sf.net TuLiP] - python-based toolbox for temporal logic planning and controller synthesis
During the course, we will access these programs on a remote machine using ssh. For some parts of the course it will be useful to have a local installation of MATLAB that can be used for visualizing some simulation results.

If you would like to install the software on your own, here are some basic directions for installing the two packages:
* Spin: if you are using Windows, you can download a [http://spinroot.com/spin/Bin/index.html binary installation]. For Mac's, you need to compile from source. For this you will need a C compiler, such as the one that is part of the [https://developer.apple.com/technologies/tools/ Xcode developer toolbox]
* TuLiP: you will need a python installation (2.6 or greater) with SciPy (0.9 or greater) installed. You might consider using the [http://enthought.com Enthought Python distribution]. Once you have scipy installed, you will need to install several other python packages, including cvxopt and yices. A [http://sourceforge.net/apps/mediawiki/tulip-control/index.php?title=Main_Page list of required package] is available on the TuLiP project page.

[[Category:Courses]]
[[Category:2012-13 Courses]]

EECI 2013: Algorithmic Verification of Hybrid Systems

2013-03-16T09:11:56Z

Utopcu: Created page with "{{eeci-sp13 header|prev=Deductive Verification|next=Protocol Synthesis}} This lecture focuses on the verification of hybrid systems. We first discuss finite-state under- and ..."

EECI 2013: Model Checking

2013-03-16T08:53:07Z

Utopcu: /* Lecture Materials */

{{eeci-sp13 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 the [[EECI 2012: Computer Session: Spin|Spin]] lecture) and discuss the computational complexity of model checking.

== Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/eeci13/L4_model-checking-2013.pdf Model Checking and Logic Synthesis] (Presentation and notation follow that in "Model Checking" chapter 5.2 by Baier and Katoen.)

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

EECI 2013: Automata Theory

2013-03-16T08:38:26Z

Utopcu: /* Lecture Materials */

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

== Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/eeci13/L2_automata-theory-2013.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 ==
* [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.

Group Schedule, Summer 2012

2012-06-08T04:35:43Z

Utopcu: /* Week 13: 10-14 September */

This page contains information about various upcoming events that are of interest to the group. __NOTOC__
{| width=60%
|- valign=top
| width=50% |
* [http://www.cds.caltech.edu/~murray/calendar.html Richard's calendar (travel)]
| width=50% |
* [[Group Schedule, Spring 2012]]
|}

The schedule for group and subgroup meetings is given below. Everyone should sign up for times to talk in the subgroup meetings.

{| width=100% border=1
|- valign=top
| width=30% |

=== Week 1: 18-22 June ===

'''Biocircuits: 21 Jun (Thu), 10 am - 12 pm'''
* SURF introductions (40 min)
* Ophelia (20-30 min)
* Shaunak K (10-15 min)
* Lab updates

'''Group meeting: 21 Jun (Thu), 12-1'''
* Richard (research overview)

'''NCS/Robotics: 21 Jun (Thu), 4-6 pm'''
* SURF introductions (20 min)
* Eric (15-20 min)
* Clemens (15-20 min)
* Project updates

<hr>
* Richard out of town Mon-Tue
* SURF students start on Tue
| width=30% |

=== Week 2: 25-29 June ===
* American Control Conference (Montreal)
* Richard out of town all week
| width=30% |

=== Week 3: 2-6 July ===
* Richard out of town all week
* Institute holiday on Wed
|- valign=top
|

=== Week 4: 9-13 July ===
'''Biocircuits: 10 Jul (Tue), 10 am - 12 pm'''
* Meeting may shift to Mon, 10a-12p
* Victoria (25-30 min)
* Anu (10-15 min)
* Jongmin (10-15 min)
* Instrument: Microscope/CellASIC
* Lab updates

'''Group meeting: 13 Jul (Fri), 12-1:15'''
* Tim Sullivan (Owhadi group)

'''NCS/Robotics: 13 Jul (Fri), 1:15-3 pm'''
* Stephanie (15-20 min)
* Research update (15-20 min)
* Research update (15-20 min)
* Project updates

<hr>
* Richard out of town Tue pm - Thu (Living Foundries PI meeting)
|

=== Week 5: 16-20 July ===
'''Biocircuits: 17 Jul (Tue), 10 am - 12 pm'''
* Anu (30-40 min)
* Zach (10-15 min)
* SURF: Vinay V (10-15 min)
* SURF update (10-15 min)
* Instrument: Computing
* Lab updates

'''NCS/Robotics: 18 Jul (Wed), 4-6 pm'''
* Mumu (15-20 min)
* Research update (15-20 min)
* SURF update (10-15 min)
* SURF update (10-15 min)
* Project updates

'''Group meeting: 19 Jul (Thu), 12-1:15'''
* Chin-Lin Guo (BE)
<hr>
* Shaunak K SURF presentation
|

=== Week 6: 23-27 July ===
'''Biocircuits: 24 Jul (Tue), 10 am - 12 pm'''
* Emzo (30-40 min)
* Enoch (10-15 min)
* SURF update (10-15 min)
* SURF update (10-15 min)
* Instrument: FACSCalibur/Quanta
* Lab updates

'''Group meeting: 25 Jul (Wed), 12-1:15'''
* Open

'''NCS/Robotics: 25 Jul (Wed), 4-6 pm'''
* Pavithra (15-20 min)
* Clemens (10-15 min)
* SURF update (10-15 min)
* SURF update (10-15 min)
* Project updates
<hr>
* Richard out of town Thu-Fri
|- valign=top
|

=== Week 7: 30 July - 3 August ===
'''Biocircuits: 31 Jul (Tue), 12-1:30 pm'''
* Lunch meeting; may shift to Thu
* Research presentation (30-40 min)
* SURF update (10-15 min)
* SURF update (10-15 min)
* Lab updates

'''NCS/Robotics: 1 Aug (Wed), 12-1:30 pm'''
* Lunch meeting; may shift to Thu
* Eric (15-20 min)
* Ufuk (15-20 min)
* Project updates

<hr>
* KISS workshop; Richard unavailable
|

=== Week 8: 6-10 August ===
'''Biocircuits: 7 Aug (Tue), 10 am - 12 pm'''
* Dan (30-40 min)
* Victoria (10-15 min)
* Marcella (10-15 min)
* Instrument: Victor X3/BioTek H1MF
* Lab updates

'''Group meeting: 8 Aug (Wed), 12-1:15'''
* Open

'''NCS/Robotics: 8 Aug (Wed), 4-6 pm'''
* Research update (15-20 min)
* Research update (15-20 min)
* Research update (15-20 min)
* Project updates

|

=== Week 9: 13-17 August ===
* Richard out all week
|- valign=top
|

=== Week 10: 20-24 August ===
'''Biocircuits: 22 Aug (Wed), 10 am - 12 pm'''
* Research presentation [non-MPP] (30-40 min)
* Research presentation [non-MPP] (10-15 min)
* Research update [non-MPP] (10-15 min)
* Instrument: freezers/cold room
* Lab updates

'''NCS/Robotics: 22 Aug (Wed), 4-6 pm'''
* Research update (15-20 min)
* Research update (15-20 min)
* Research update (15-20 min)
* Project updates

'''Group meeting: 23 Aug (Thu), 12-1:15'''
* Lea Goentoro (Bi)
<hr>
* MPP retreat, Sun-Tue
|

=== Week 11: 27-31 August ===
'''Biocircuits: 28 Aug (Tue), 10 am - 12 pm'''
* Jongmin (30-40 min)
* Research update (10-15 min)
* Research update (10-15 min)
* Instruments: Nanodrop/electroporator
* Lab updates

'''NCS/Robotics: 29 Aug (Wed), 4-6 pm'''
* Mumu (15-20 min)
* Research update (15-20 min)
* Research update (15-20 min)
* Project updates

'''Group meeting: 30 Aug (Thu), 12-1:15'''
* Open
<hr>
* Richard out of town on Fri
|

=== Week 12: 3-7 September ===
'''Biocircuits: 4 Sep (Tue), 10 am - 12 pm'''
* Marcella (30-40 min)
* Research update (10-15 min)
* Research update (10-15 min)
* Instrument: gel rigs/gel imager
* Lab updates

'''NCS/Robotics: 5 Sep (Wed), 4-6 pm'''
* Research update (15-20 min)
* Research update (15-20 min)
* Research update (15-20 min)
* Project updates

'''Group meeting: 6 Sep (Thu), 12-1:15'''
* Open
<hr>
* Institute holiday on Mon
|- valign=top
|

=== Week 13: 10-14 September ===
'''Biocircuits: 11 Sep (Tue), 10 am - 12 pm'''
* Zach (30-40 min)
* Research update (10-15 min)
* Research update (10-15 min)
* Instrument: PCR machines/centrifuges
* Lab updates

'''NCS/Robotics: 12 Sep (Wed), 4-6 pm'''
* Ufuk (15-20 min)
* Research update (15-20 min)
* Research update (15-20 min)
* Project updates

'''Group meeting: 13 Sep (Thu), 12-1:15'''
* Open
<hr>
* Richard out on Fri
|

=== Week 14: 17-21 September ===
* Richard out all week
|
=== Week 15: 24-28 September ===
'''Biocircuits: 25 Sep (Tue), 10 am - 12 pm'''
* Enoch (30-40 min)
* Emzo (10-15 min)
* Dan (10-15 min)
* Lab updates

'''NCS/Robotics: 26 Sep (Wed), 4-6 pm'''
* Stephanie (15-20 min)
* Research update (15-20 min)
* Research update (15-20 min)
* Project updates

'''Group meeting: 26 Sep (Thu), 12-1:15'''
* Open
<hr>
* Richard out on Mon
|}

Group Schedule, Summer 2012

2012-06-08T04:35:00Z

Utopcu: /* Week 7: 30 July - 3 August */

This page contains information about various upcoming events that are of interest to the group. __NOTOC__
{| width=60%
|- valign=top
| width=50% |
* [http://www.cds.caltech.edu/~murray/calendar.html Richard's calendar (travel)]
| width=50% |
* [[Group Schedule, Spring 2012]]
|}

The schedule for group and subgroup meetings is given below. Everyone should sign up for times to talk in the subgroup meetings.

{| width=100% border=1
|- valign=top
| width=30% |

=== Week 1: 18-22 June ===

'''Biocircuits: 21 Jun (Thu), 10 am - 12 pm'''
* SURF introductions (40 min)
* Ophelia (20-30 min)
* Shaunak K (10-15 min)
* Lab updates

'''Group meeting: 21 Jun (Thu), 12-1'''
* Richard (research overview)

'''NCS/Robotics: 21 Jun (Thu), 4-6 pm'''
* SURF introductions (20 min)
* Eric (15-20 min)
* Clemens (15-20 min)
* Project updates

<hr>
* Richard out of town Mon-Tue
* SURF students start on Tue
| width=30% |

=== Week 2: 25-29 June ===
* American Control Conference (Montreal)
* Richard out of town all week
| width=30% |

=== Week 3: 2-6 July ===
* Richard out of town all week
* Institute holiday on Wed
|- valign=top
|

=== Week 4: 9-13 July ===
'''Biocircuits: 10 Jul (Tue), 10 am - 12 pm'''
* Meeting may shift to Mon, 10a-12p
* Victoria (25-30 min)
* Anu (10-15 min)
* Jongmin (10-15 min)
* Instrument: Microscope/CellASIC
* Lab updates

'''Group meeting: 13 Jul (Fri), 12-1:15'''
* Tim Sullivan (Owhadi group)

'''NCS/Robotics: 13 Jul (Fri), 1:15-3 pm'''
* Stephanie (15-20 min)
* Research update (15-20 min)
* Research update (15-20 min)
* Project updates

<hr>
* Richard out of town Tue pm - Thu (Living Foundries PI meeting)
|

=== Week 5: 16-20 July ===
'''Biocircuits: 17 Jul (Tue), 10 am - 12 pm'''
* Anu (30-40 min)
* Zach (10-15 min)
* SURF: Vinay V (10-15 min)
* SURF update (10-15 min)
* Instrument: Computing
* Lab updates

'''NCS/Robotics: 18 Jul (Wed), 4-6 pm'''
* Mumu (15-20 min)
* Research update (15-20 min)
* SURF update (10-15 min)
* SURF update (10-15 min)
* Project updates

'''Group meeting: 19 Jul (Thu), 12-1:15'''
* Chin-Lin Guo (BE)
<hr>
* Shaunak K SURF presentation
|

=== Week 6: 23-27 July ===
'''Biocircuits: 24 Jul (Tue), 10 am - 12 pm'''
* Emzo (30-40 min)
* Enoch (10-15 min)
* SURF update (10-15 min)
* SURF update (10-15 min)
* Instrument: FACSCalibur/Quanta
* Lab updates

'''Group meeting: 25 Jul (Wed), 12-1:15'''
* Open

'''NCS/Robotics: 25 Jul (Wed), 4-6 pm'''
* Pavithra (15-20 min)
* Clemens (10-15 min)
* SURF update (10-15 min)
* SURF update (10-15 min)
* Project updates
<hr>
* Richard out of town Thu-Fri
|- valign=top
|

=== Week 7: 30 July - 3 August ===
'''Biocircuits: 31 Jul (Tue), 12-1:30 pm'''
* Lunch meeting; may shift to Thu
* Research presentation (30-40 min)
* SURF update (10-15 min)
* SURF update (10-15 min)
* Lab updates

'''NCS/Robotics: 1 Aug (Wed), 12-1:30 pm'''
* Lunch meeting; may shift to Thu
* Eric (15-20 min)
* Ufuk (15-20 min)
* Project updates

<hr>
* KISS workshop; Richard unavailable
|

=== Week 8: 6-10 August ===
'''Biocircuits: 7 Aug (Tue), 10 am - 12 pm'''
* Dan (30-40 min)
* Victoria (10-15 min)
* Marcella (10-15 min)
* Instrument: Victor X3/BioTek H1MF
* Lab updates

'''Group meeting: 8 Aug (Wed), 12-1:15'''
* Open

'''NCS/Robotics: 8 Aug (Wed), 4-6 pm'''
* Research update (15-20 min)
* Research update (15-20 min)
* Research update (15-20 min)
* Project updates

|

=== Week 9: 13-17 August ===
* Richard out all week
|- valign=top
|

=== Week 10: 20-24 August ===
'''Biocircuits: 22 Aug (Wed), 10 am - 12 pm'''
* Research presentation [non-MPP] (30-40 min)
* Research presentation [non-MPP] (10-15 min)
* Research update [non-MPP] (10-15 min)
* Instrument: freezers/cold room
* Lab updates

'''NCS/Robotics: 22 Aug (Wed), 4-6 pm'''
* Research update (15-20 min)
* Research update (15-20 min)
* Research update (15-20 min)
* Project updates

'''Group meeting: 23 Aug (Thu), 12-1:15'''
* Lea Goentoro (Bi)
<hr>
* MPP retreat, Sun-Tue
|

=== Week 11: 27-31 August ===
'''Biocircuits: 28 Aug (Tue), 10 am - 12 pm'''
* Jongmin (30-40 min)
* Research update (10-15 min)
* Research update (10-15 min)
* Instruments: Nanodrop/electroporator
* Lab updates

'''NCS/Robotics: 29 Aug (Wed), 4-6 pm'''
* Mumu (15-20 min)
* Research update (15-20 min)
* Research update (15-20 min)
* Project updates

'''Group meeting: 30 Aug (Thu), 12-1:15'''
* Open
<hr>
* Richard out of town on Fri
|

=== Week 12: 3-7 September ===
'''Biocircuits: 4 Sep (Tue), 10 am - 12 pm'''
* Marcella (30-40 min)
* Research update (10-15 min)
* Research update (10-15 min)
* Instrument: gel rigs/gel imager
* Lab updates

'''NCS/Robotics: 5 Sep (Wed), 4-6 pm'''
* Research update (15-20 min)
* Research update (15-20 min)
* Research update (15-20 min)
* Project updates

'''Group meeting: 6 Sep (Thu), 12-1:15'''
* Open
<hr>
* Institute holiday on Mon
|- valign=top
|

=== Week 13: 10-14 September ===
'''Biocircuits: 11 Sep (Tue), 10 am - 12 pm'''
* Zach (30-40 min)
* Research update (10-15 min)
* Research update (10-15 min)
* Instrument: PCR machines/centrifuges
* Lab updates

'''NCS/Robotics: 12 Sep (Wed), 4-6 pm'''
* Research update (15-20 min)
* Research update (15-20 min)
* Research update (15-20 min)
* Project updates

'''Group meeting: 13 Sep (Thu), 12-1:15'''
* Open
<hr>
* Richard out on Fri
|

=== Week 14: 17-21 September ===
* Richard out all week
|
=== Week 15: 24-28 September ===
'''Biocircuits: 25 Sep (Tue), 10 am - 12 pm'''
* Enoch (30-40 min)
* Emzo (10-15 min)
* Dan (10-15 min)
* Lab updates

'''NCS/Robotics: 26 Sep (Wed), 4-6 pm'''
* Stephanie (15-20 min)
* Research update (15-20 min)
* Research update (15-20 min)
* Project updates

'''Group meeting: 26 Sep (Thu), 12-1:15'''
* Open
<hr>
* Richard out on Mon
|}

EECI 2012: Deductive Verification of Hybrid Systems

2012-05-16T08:11:49Z

Utopcu: /* Lecture Materials */

{{eeci-sp12 header|prev=Computer Session: Spin|next=Algorithmic Verification}}

This lecture focuses on the verification of hybrid systems using deductive (theorem proving) methods. We describe hybrid systems that combine continuous and discrete states. We then describe two methods for deductive verification. First, we discuss a computational procedure for constructing Lyapunov-type functions (e.g., barrier certificates) that witness the fact that a hybrid system satisfies certain temporal specifications. Second, we consider control protocols for cooperation and decision making in multi-agent systems, as illustrated by the RoboFlag example introduced in the first lecture. We show how to implement a simple protocol for distributed target assignment in a simplified version of the problem (the "RoboFlag drill") and prove stability of the protocol.

== Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/L5_deductive-16May12.pdf Deductive Verification of Hybrid Systems]

Some of the slides are from a short course ([http://www.cds.caltech.edu/~utopcu/index.php/Short_Course:_Quantitative_Local_Analysis_of_Nonlinear_Systems_Using_Sum-of-Squares_Decompositions Quantitative Local Analysis of Nonlinear Systems Using Sum-of-Squares Decompositions]) by Balas, Packard, Seiler, and Topcu.

== Further Reading ==
* [http://resolver.caltech.edu/CaltechETD:etd-05272005-144358 Stephen Prajna's dissertation] on verifying temporal properties for hybrid dynamical systems. 
* [http://www.cds.caltech.edu/~utopcu/images//9/9b/TPSB-CSM-2010.pdf Help on SOS]: a paper on the very basics of sum-of-squares programming and their use in nonlinear system verification.
* [http://arxiv.org/abs/math.OC/0103170 Minimizing Polynomial Functions] by P. Parrilo and B. Sturmfels on global optimization of polynomial functions and Positivstellensatz (generalizations of the S-procedure). 
* [http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=1271797 A Computation and Control Language for Multi-Vehicle Systems], E. Klavins. Int’l Conference on Robotics and Automation, 2004. 
* [http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=1269132 Distributed Algorithms for Cooperative Control], E. Klavins and R. M. Murray. ''IEEE Pervasive Computing'', 2004. 

== Additional Materials ==

EECI 2012: Deductive Verification of Hybrid Systems

2012-05-16T08:10:01Z

Utopcu: /* Further Reading */

{{eeci-sp12 header|prev=Computer Session: Spin|next=Algorithmic Verification}}

This lecture focuses on the verification of hybrid systems using deductive (theorem proving) methods. We describe hybrid systems that combine continuous and discrete states. We then describe two methods for deductive verification. First, we discuss a computational procedure for constructing Lyapunov-type functions (e.g., barrier certificates) that witness the fact that a hybrid system satisfies certain temporal specifications. Second, we consider control protocols for cooperation and decision making in multi-agent systems, as illustrated by the RoboFlag example introduced in the first lecture. We show how to implement a simple protocol for distributed target assignment in a simplified version of the problem (the "RoboFlag drill") and prove stability of the protocol.

== Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/L5_deductive-16May12.pdf Deductive Verification of Hybrid Systems]

== Further Reading ==
* [http://resolver.caltech.edu/CaltechETD:etd-05272005-144358 Stephen Prajna's dissertation] on verifying temporal properties for hybrid dynamical systems. 
* [http://www.cds.caltech.edu/~utopcu/images//9/9b/TPSB-CSM-2010.pdf Help on SOS]: a paper on the very basics of sum-of-squares programming and their use in nonlinear system verification.
* [http://arxiv.org/abs/math.OC/0103170 Minimizing Polynomial Functions] by P. Parrilo and B. Sturmfels on global optimization of polynomial functions and Positivstellensatz (generalizations of the S-procedure). 
* [http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=1271797 A Computation and Control Language for Multi-Vehicle Systems], E. Klavins. Int’l Conference on Robotics and Automation, 2004. 
* [http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=1269132 Distributed Algorithms for Cooperative Control], E. Klavins and R. M. Murray. ''IEEE Pervasive Computing'', 2004. 

== Additional Materials ==

EECI 2012: Computer Session: Spin

2012-05-15T14:49:11Z

Utopcu:

{{eeci-sp12 header|prev=Model Checking|next=Deductive Verification}}

{{righttoc}}
Hands-on model checking exercises using SPIN.

== Lecture Materials ==
* [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/C1_spin-15May12.pdf Lecture slides]
* Example promela files: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/lights_simple.pml lights_simple.pml], [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/lights_distributed.pml lights_distributed.pml], [http://www.cds.caltech.edu/~utopcu/EECI2012/lights_synthesis.pml lights_synthesis.pml]
* [http://www.cds.caltech.edu/~utopcu/eeci2011/SPIN_cheat_sheet.pdf Sample SPIN commands]

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

== Additional Materials ==
* [http://spinroot.com/spin/whatispin.html SPIN web site] 
* [http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/ LTL2BA] - a web page (and program) for converting LTL formulas to Buchi automata.

EECI 2012: Receding Horizon Temporal Logic Planning

2012-05-14T10:24:14Z

Utopcu:

EECI 2012: Receding Horizon Temporal Logic Planning

2012-05-14T10:19:57Z

Utopcu:

EECI 2012: Receding Horizon Temporal Logic Planning

2012-05-14T10:17:45Z

Utopcu:

{{AFRL12 header|prev=Synthesis of Reactive Control Protocols |next=TuLiP}}

The first part of this lecture introduces the receding horizon temporal logic planning. Introductory material on high computational complexity of reactive control protocol synthesis is followed by the statement and discussion of a main result and a small example. We discuss implementation details, further extensions, and a hierarchical control structure that utilizes the proposed receding horizon temporal logic planning procedure. In the second part, we present some of our recent results on the compositional synthesis of distributed, reactive control protocols.

{{righttoc}}

== Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/EECI2012/L8_rhtlp_18May12.pdf Receding Horizon Temporal Logic Planning and Compositional Synthesis]

== Further Reading and Additional Information ==
* [http://www.cds.caltech.edu/~utopcu/images//4/4d/WTM-itac10R.pdf Receding horizon temporal logic planning],T. Wongpiromsarn, U. Topcu, and R. Murray, submitted to IEEE Transactions on Automatic Control, 2010. Details on the receding horizon temporal logic planning. 
* [http://www.cds.caltech.edu/~murray/wiki/index.php/EECI08:_Optimization-Based_Control Optimization based control]. A page prepared for EECI 2008 with information and material on basic receding horizon control.
* [http://control.ee.ethz.ch/~mpt/ Multiparametric Toolbox] The Multi-Parametric Toolbox (MPT) is a free Matlab toolbox for design, analysis and deployment of optimal controllers for constrained linear, nonlinear and hybrid systems. [http://www.cds.caltech.edu/tulip The receding horizon temporal logic planning toolbox] uses the polytope manipulation (intersection, union, set difference, projection, etc.) functionalities of MPT. 

* [http://www.cds.caltech.edu/~utopcu/images//9/98/WTM-aaai10.pdf Automatic synthesis of robust embedded control software], T. Wongpiromsarn, U. Topcu, and R. Murray, AAAI 2010 Spring Symposium on Embedded Reasoning: Intelligence in Embedded Systems, 2010. Details on the abstraction procedure covered in this lecture. 

* [http://www.mpc.berkeley.edu/mpc-course-material/BBMbook_Cambridge.pdf?attredirects=0&d=1 Predictive Control]: A book draft by Bemporap, Borrelli, and Morari. Details on some of the ideas in the implementation of the abstraction procedure presented in the slides can be found in this book.

EECI 2012: Receding Horizon Temporal Logic Planning

2012-05-14T10:15:50Z

Utopcu:

{{AFRL12 header|prev=Synthesis of Reactive Control Protocols |next=TuLiP}}

The first part of this lecture introduces the receding horizon temporal logic planning. Introductory material on high computational complexity of reactive control protocol synthesis is followed by the statement and discussion of a main result and a small example. We discuss implementation details, further extensions, and a hierarchical control structure that utilizes the proposed receding horizon temporal logic planning procedure. In the second part, we present some of our recent results on the compositional synthesis of distributed, reactive control protocols.

{{righttoc}}

== Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/EECI2012/L8_rhtlp_18May12.pdf Receding Horizon Temporal Logic Planning]

== Further Reading and Additional Information ==
* [http://www.cds.caltech.edu/~utopcu/images//4/4d/WTM-itac10R.pdf Receding horizon temporal logic planning],T. Wongpiromsarn, U. Topcu, and R. Murray, submitted to IEEE Transactions on Automatic Control, 2010. Details on the receding horizon temporal logic planning. 
* [http://www.cds.caltech.edu/~murray/wiki/index.php/EECI08:_Optimization-Based_Control Optimization based control]. A page prepared for EECI 2008 with information and material on basic receding horizon control.
* [http://control.ee.ethz.ch/~mpt/ Multiparametric Toolbox] The Multi-Parametric Toolbox (MPT) is a free Matlab toolbox for design, analysis and deployment of optimal controllers for constrained linear, nonlinear and hybrid systems. [http://www.cds.caltech.edu/tulip The receding horizon temporal logic planning toolbox] uses the polytope manipulation (intersection, union, set difference, projection, etc.) functionalities of MPT. 

* [http://www.cds.caltech.edu/~utopcu/images//9/98/WTM-aaai10.pdf Automatic synthesis of robust embedded control software], T. Wongpiromsarn, U. Topcu, and R. Murray, AAAI 2010 Spring Symposium on Embedded Reasoning: Intelligence in Embedded Systems, 2010. Details on the abstraction procedure covered in this lecture. 

* [http://www.mpc.berkeley.edu/mpc-course-material/BBMbook_Cambridge.pdf?attredirects=0&d=1 Predictive Control]: A book draft by Bemporap, Borrelli, and Morari. Details on some of the ideas in the implementation of the abstraction procedure presented in the slides can be found in this book.

HYCON-EECI, Spring 2012

2012-05-14T10:14:03Z

Utopcu: Undo revision 14048 by Utopcu (Talk)

<table width="100%" cellspacing=0>
<tr valign=top>
<td rowspan=4 align=center> [[Image:eecilogo.png|90px]]</td>
<td align=center>Specification, Design, and Verification  </td>
<td rowspan=4 align=center"> [[Image:cdslogo.png|90px]]</td></tr>
<tr><td align=center>of Distributed Embedded Systems   </td></tr>
<tr valign=top><td align=center> Richard M. Murray, Ufuk Topcu, and Nok Wongpiromsarn </td></tr>
<tr valign=top><td align=center>14-18 May 2012, L'Aquila (Italy)</td></tr>
</table> __NOTOC__

== Course Description ==
Increases in fast and inexpensive computing and communications have enabled a new generation of information-rich control systems that rely on multi-threaded networked execution, distributed optimization, sensor fusion and protocol stacks in increasingly sophisticated ways. This course will provide working knowledge of a collection of methods and tools for specifying, designing and verifying networked control systems. We combine methods from computer science (temporal logic, model checking, synthesis of control protocols) with those from dynamical systems and control (Lyapunov functions, trajectory generation, receding horizon control) to analyze and design partially asynchronous control protocols for continuous systems. In addition to introducing the mathematical techniques required to formulate problems and prove properties, we also describe a software toolbox (TuLiP) that is designed for analyzing and synthesizing hybrid control systems using linear temporal logic and robust performance specifications.

== Course information ==
* Instructors: [http://www.cds.caltech.edu/~murray/wiki/Main_Page Richard M. Murray] (Caltech, CDS) and [http://www.cds.caltech.edu/~utopcu/index.php/Main_Page Ufuk Topcu] (Caltech, CDS), and [http://www.cds.caltech.edu/~nok/ Nok Wongpiromsarn] (MIT-Singapore)
* Date and location: 14-18 May 2012, L'Aquila (Italy)
* Sponsor: [http://www.eeci-institute.eu/GSC2011 HYCON-EECI Graduate School on Control]

== Lecture Schedule ==

The schedule below lists the lectures that will be given as part of the course. Each lecture will last approximately 90 minutes. The individual lecture pages give an overview of the lecture and links to additional information.

{|border=1 cellpadding=2
|-
|align=center|Lec
|align=center|Date/time
|Title
|Topics
{{eeci12 entry|L1|RM|Mon, 9:00|Introduction: Protocol-Based Control Systems|
* Introduction to networked control systems (NCS)
* Overview of control "protocols"
* Examples: Alice, RoboFlag
}}
{{eeci12 entry|L2|NW|Mon, 11:00|Automata Theory|
* Finite transition systems
* Paths, traces and composition of finite transition systems
* Linear time properties; safety and liveness
* Examples: traffic light
}}
{{eeci12 entry|L3|UT|Mon, 14:00|Temporal Logic|
* Linear temporal logic
* Omega regular properties
* Buchi automata, representation of LTL using NBA
* Examples: traffic light, (RoboFlag), autonomous driving
}}
{{eeci12 entry|L4|NW|Mon, 16:00|Model Checking and Logic Synthesis|
* Basic concepts in model checking
* Use of model checking for logic synthesis
* Examples: traffic light, farmer puzzle
}}
{{eeci12 entry|C1|RM|Tue, 14:00 Tue, 16:00|Computer Session: Spin|
* Introduction to Promela and Spin (statements, processes, messages)
* Verification examples: traffic light, distributed traffic light, gcdrive
* Synthesis examples: traffic light, farmer puzzle, robot navigation
}}
{{eeci12 entry|L5|RM|Wed, 9:00|Deductive Verification of Hybrid Systems|
* Brief introduction to hybrid systems and verification techniques (deductive, algorithmic)
* Deductive verification using barrier certificates
* Guarded command languages and CCL for asynchronous control protocols
* Examples: multi-agent systems, RoboFlag
}}
{{eeci12 entry|L6|UT|Wed, 11:00|Algorithmic Verification of Hybrid Systems|
* Abstraction hierarchies for control systems
* Finite state abstractions (discretization) and model checking
* Discretization of continuous state systems
* Approximate bi-simulation (if time)
* Examples: gear changing (?), ???
}}
{{eeci12 entry|L7|NW|Wed, 14:00|Synthesis of Reactive Control Protocols|
* Open system and reactive system synthesis
* Satisfiability, realizability
* Game structures, reachability/safety games
* Mu-calculus (if time) and GR(1) games
* Examples: runner-blocker
}}
{{eeci12 entry|C2|NW|Thu, 9:00 Thu, 11:00|Computer Session: TuLiP|
* Introduction to TuLiP
* Synthesis of protocols for discrete systems
* Discretization of continuous systems (and protocol synthesis)
* Examples: reactive motion planning
}}
{{eeci12 entry|L8|UT|Fri, 9:00|Receding Horizon Temporal Logic Planning|
* Receding horizon control
* Distributed control
* Examples: reactive motion planning, electric power systems (distributed)
}}
{{eeci12 entry|L9|RM|Fri, 11:00|Extensions, Applications, Open Questions|
* Review of control trends and course contents
* Discussion of open problem areas and preliminary results
** Optimization-based techniques
** Probabilistic techniques
** Others: Robustness, switching systems, timed systems
* Examples: robot motion planning, electric power systems (timed)
}}
|}

== Software Installation ==

We will make use of two programs during the lab sessions:
* [http://spinroot.com Spin] - model checker for formal verification of distributed systems
* [http://tulip-control.sf.net TuLiP] - python-based toolbox for temporal logic planning and controller synthesis
During the course, we will access these programs on a remote machine using ssh. For some parts of the course it will be useful to have a local installation of MATLAB that can be used for visualizing some simulation results.

If you would like to install the software on your own, here are some basic directions for installing the two packages:
* Spin: if you are using Windows, you can download a [http://spinroot.com/spin/Bin/index.html binary installation]. For Mac's, you need to compile from source. For this you will need a C compiler, such as the one that is part of the [https://developer.apple.com/technologies/tools/ Xcode developer toolbox]
* TuLiP: you will need a python installation (2.6 or greater) with SciPy (0.9 or greater) installed. You might consider using the [http://enthought.com Enthought Python distribution]. Once you have scipy installed, you will need to install several other python packages, including cvxopt and yices. A [http://sourceforge.net/apps/mediawiki/tulip-control/index.php?title=Main_Page list of required package] is available on the TuLiP project page.

[[Category:Courses]]
[[Category:2011-12 Courses]]

HYCON-EECI, Spring 2012

2012-05-14T10:12:40Z

Utopcu: /* Lecture Schedule */

<table width="100%" cellspacing=0>
<tr valign=top>
<td rowspan=4 align=center> [[Image:eecilogo.png|90px]]</td>
<td align=center>Specification, Design, and Verification  </td>
<td rowspan=4 align=center"> [[Image:cdslogo.png|90px]]</td></tr>
<tr><td align=center>of Distributed Embedded Systems   </td></tr>
<tr valign=top><td align=center> Richard M. Murray, Ufuk Topcu, and Nok Wongpiromsarn </td></tr>
<tr valign=top><td align=center>14-18 May 2012, L'Aquila (Italy)</td></tr>
</table> __NOTOC__

== Course Description ==
Increases in fast and inexpensive computing and communications have enabled a new generation of information-rich control systems that rely on multi-threaded networked execution, distributed optimization, sensor fusion and protocol stacks in increasingly sophisticated ways. This course will provide working knowledge of a collection of methods and tools for specifying, designing and verifying networked control systems. We combine methods from computer science (temporal logic, model checking, synthesis of control protocols) with those from dynamical systems and control (Lyapunov functions, trajectory generation, receding horizon control) to analyze and design partially asynchronous control protocols for continuous systems. In addition to introducing the mathematical techniques required to formulate problems and prove properties, we also describe a software toolbox (TuLiP) that is designed for analyzing and synthesizing hybrid control systems using linear temporal logic and robust performance specifications.

== Course information ==
* Instructors: [http://www.cds.caltech.edu/~murray/wiki/Main_Page Richard M. Murray] (Caltech, CDS) and [http://www.cds.caltech.edu/~utopcu/index.php/Main_Page Ufuk Topcu] (Caltech, CDS), and [http://www.cds.caltech.edu/~nok/ Nok Wongpiromsarn] (MIT-Singapore)
* Date and location: 14-18 May 2012, L'Aquila (Italy)
* Sponsor: [http://www.eeci-institute.eu/GSC2011 HYCON-EECI Graduate School on Control]

== Lecture Schedule ==

The schedule below lists the lectures that will be given as part of the course. Each lecture will last approximately 90 minutes. The individual lecture pages give an overview of the lecture and links to additional information.

{|border=1 cellpadding=2
|-
|align=center|Lec
|align=center|Date/time
|Title
|Topics
{{eeci12 entry|L1|RM|Mon, 9:00|Introduction: Protocol-Based Control Systems|
* Introduction to networked control systems (NCS)
* Overview of control "protocols"
* Examples: Alice, RoboFlag
}}
{{eeci12 entry|L2|NW|Mon, 11:00|Automata Theory|
* Finite transition systems
* Paths, traces and composition of finite transition systems
* Linear time properties; safety and liveness
* Examples: traffic light
}}
{{eeci12 entry|L3|UT|Mon, 14:00|Temporal Logic|
* Linear temporal logic
* Omega regular properties
* Buchi automata, representation of LTL using NBA
* Examples: traffic light, (RoboFlag), autonomous driving
}}
{{eeci12 entry|L4|NW|Mon, 16:00|Model Checking and Logic Synthesis|
* Basic concepts in model checking
* Use of model checking for logic synthesis
* Examples: traffic light, farmer puzzle
}}
{{eeci12 entry|C1|RM|Tue, 14:00 Tue, 16:00|Computer Session: Spin|
* Introduction to Promela and Spin (statements, processes, messages)
* Verification examples: traffic light, distributed traffic light, gcdrive
* Synthesis examples: traffic light, farmer puzzle, robot navigation
}}
{{eeci12 entry|L5|RM|Wed, 9:00|Deductive Verification of Hybrid Systems|
* Brief introduction to hybrid systems and verification techniques (deductive, algorithmic)
* Deductive verification using barrier certificates
* Guarded command languages and CCL for asynchronous control protocols
* Examples: multi-agent systems, RoboFlag
}}
{{eeci12 entry|L6|UT|Wed, 11:00|Algorithmic Verification of Hybrid Systems|
* Abstraction hierarchies for control systems
* Finite state abstractions (discretization) and model checking
* Discretization of continuous state systems
* Approximate bi-simulation (if time)
* Examples: gear changing (?), ???
}}
{{eeci12 entry|L7|NW|Wed, 14:00|Synthesis of Reactive Control Protocols|
* Open system and reactive system synthesis
* Satisfiability, realizability
* Game structures, reachability/safety games
* Mu-calculus (if time) and GR(1) games
* Examples: runner-blocker
}}
{{eeci12 entry|C2|NW|Thu, 9:00 Thu, 11:00|Computer Session: TuLiP|
* Introduction to TuLiP
* Synthesis of protocols for discrete systems
* Discretization of continuous systems (and protocol synthesis)
* Examples: reactive motion planning
}}
{{eeci12 entry|L8|UT|Fri, 9:00|Receding Horizon Temporal Logic Planning and Compositional Synthesis|
* Receding horizon control
* Distributed control
* Examples: reactive motion planning, electric power systems (distributed)
}}
{{eeci12 entry|L9|RM|Fri, 11:00|Extensions, Applications, Open Questions|
* Review of control trends and course contents
* Discussion of open problem areas and preliminary results
** Optimization-based techniques
** Probabilistic techniques
** Others: Robustness, switching systems, timed systems
* Examples: robot motion planning, electric power systems (timed)
}}
|}

== Software Installation ==

We will make use of two programs during the lab sessions:
* [http://spinroot.com Spin] - model checker for formal verification of distributed systems
* [http://tulip-control.sf.net TuLiP] - python-based toolbox for temporal logic planning and controller synthesis
During the course, we will access these programs on a remote machine using ssh. For some parts of the course it will be useful to have a local installation of MATLAB that can be used for visualizing some simulation results.

If you would like to install the software on your own, here are some basic directions for installing the two packages:
* Spin: if you are using Windows, you can download a [http://spinroot.com/spin/Bin/index.html binary installation]. For Mac's, you need to compile from source. For this you will need a C compiler, such as the one that is part of the [https://developer.apple.com/technologies/tools/ Xcode developer toolbox]
* TuLiP: you will need a python installation (2.6 or greater) with SciPy (0.9 or greater) installed. You might consider using the [http://enthought.com Enthought Python distribution]. Once you have scipy installed, you will need to install several other python packages, including cvxopt and yices. A [http://sourceforge.net/apps/mediawiki/tulip-control/index.php?title=Main_Page list of required package] is available on the TuLiP project page.

[[Category:Courses]]
[[Category:2011-12 Courses]]

EECI 2012: Algorithmic Verification of Hybrid Systems

2012-05-14T10:10:20Z

Utopcu:

{{eeci-sp12 header|prev=Deductive Verification of Hybrid Systems|next=Synthesis of Reactive Control Protocols}}

This lecture focuses on the verification of hybrid systems. We first discuss finite-state under- and over-approximations of hybrid dynamics and how these finite-state models coupled with the model checking tools can be used to verify temporal logic properties against hybrid dynamics. Then, we present a procedure for constructing finite-state, under-approximations which will later be used in the course in the synthesis of hierarchical control protocols. We finally introduce the notions of approximate bisimulations and bisimulation functions and how they can be used in verification of temporal properties.

{{righttoc}}

== Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/EECI2012/L5_abstractions_16May12.pdf Abstractions for the Analysis and Synthesis of Control Protocols for Hybrid Systems]

== Additional Material and Further Reading ==
* [http://robotics.eecs.berkeley.edu/~sastry/ee291e/lygeros.pdf Lecture Notes on Hybrid Systems] (by John Lygeros): A rough introduction to hybrid systems. Chapters 5 and 6 are on various analysis techniques relevant for this short course. 
* [http://www.cds.caltech.edu/~utopcu/images//4/4d/WTM-itac10R.pdf Receding horizon temporal logic planning],T. Wongpiromsarn, U. Topcu, and R. Murray, submitted to IEEE Transactions on Automatic Control, 2010. Details on the receding horizon temporal logic planning. 
* [http://www.cds.caltech.edu/~murray/wiki/index.php/EECI08:_Optimization-Based_Control Optimization based control]. A page prepared for EECI 2008 with information and material on basic receding horizon control.
* [http://control.ee.ethz.ch/~mpt/ Multiparametric Toolbox] The Multi-Parametric Toolbox (MPT) is a free Matlab toolbox for design, analysis and deployment of optimal controllers for constrained linear, nonlinear and hybrid systems. [http://www.cds.caltech.edu/tulip The receding horizon temporal logic planning toolbox] uses the polytope manipulation (intersection, union, set difference, projection, etc.) functionalities of MPT. 
* [http://www.cds.caltech.edu/~utopcu/images//9/98/WTM-aaai10.pdf Automatic synthesis of robust embedded control software], T. Wongpiromsarn, U. Topcu, and R. Murray, AAAI 2010 Spring Symposium on Embedded Reasoning: Intelligence in Embedded Systems, 2010. Details on the abstraction procedure covered in this lecture. 
* [http://www.mpc.berkeley.edu/mpc-course-material/BBMbook_Cambridge.pdf?attredirects=0&d=1 Predictive Control]: A book draft by Bemporap, Borrelli, and Morari. Details on some of the ideas in the implementation of the abstraction procedure presented in the slides can be found in this book.

EECI 2012: Algorithmic Verification of Hybrid Systems

2012-05-14T10:09:17Z

Utopcu:

EECI 2012: Algorithmic Verification of Hybrid Systems

2012-05-14T10:08:44Z

Utopcu:

{{eeci-sp12 header|prev=Deductive Verification of Hybrid Systems|next=Synthesis of Reactive Control Protocols}}

This lecture focuses on the verification of hybrid systems. We first discuss finite-state under- and over-approximations of hybrid dynamics and how these finite-state models coupled with the model checking tools can be used to verify temporal logic properties against hybrid dynamics. Then, we present a procedure for constructing finite-state, under-approximations which will later be used in the course in the synthesis of hierarchical control protocols. We finally introduce the notions of approximate bisimulations and bisimulation functions and how they can be used in verification of temporal properties.

{{righttoc}}

== Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/EECI2012/L5_abstractions_16May12.pdf Abstractions for the Analysis and Synthesis of Control Protocols for Hybrid Systems]

== Additional Material and Further Reading ==
* [http://www.cds.caltech.edu/~utopcu/index.php/Short_Course:_Quantitative_Local_Analysis_of_Nonlinear_Systems_Using_Sum-of-Squares_Decompositions Material on part III]. Links to software packages, slides, and notes on quantitative analysis of nonlinear systems. Shorter version is in these [http://www.cds.caltech.edu/~utopcu/cdc10vvslides/UfukTopcu.pdf slides]
* [http://etd.caltech.edu/etd/available/etd-05272005-144358/ Stephen Prajna's dissertation] on verifying temporal properties for hybrid dynamical systems. 
* [http://www.cds.caltech.edu/~utopcu/images//9/9b/TPSB-CSM-2010.pdf Help on SOS]: a paper on the very basics of sum-of-squares programming and their use in nonlinear system verification.
* [http://arxiv.org/abs/math.OC/0103170 Minimizing Polynomial Functions] by P. Parrilo and B. Sturmfels on global optimization of polynomial functions and Positivstellensatz (generalizations of the S-procedure). 
* [http://robotics.eecs.berkeley.edu/~sastry/ee291e/lygeros.pdf Lecture Notes on Hybrid Systems] (by John Lygeros): A rough introduction to hybrid systems. Chapters 5 and 6 are on various analysis techniques relevant for this short course.

EECI 2012: Algorithmic Verification of Hybrid Systems

2012-05-14T10:04:40Z

Utopcu: Created page with '{{eeci-sp12 header|prev=Deductive Verification of Hybrid Systems|next=Synthesis of Reactive Control Protocols}} This lecture focuses on the verification of hybrid systems. We fi…'

{{eeci-sp12 header|prev=Deductive Verification of Hybrid Systems|next=Synthesis of Reactive Control Protocols}}

This lecture focuses on the verification of hybrid systems. We first discuss finite-state under- and over-approximations of hybrid dynamics and how these finite-state models coupled with the model checking tools can be used to verify temporal logic properties against hybrid dynamics. Then, we move to deductive verification and a computational procedure for constructing Lyapunov-type functions (e.g., barrier certificates) which witness the fact that a hybrid system satisfies certain temporal specifications. We finally introduce the notions of approximate bisimulations and bisimulation functions and how they can be used in verification of temporal properties.

{{righttoc}}

== Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/AFRL2012/L6_Hybrid_Systems_Verification.pdf Hybrid Systems Verification]

== Additional Material and Further Reading ==
* [http://www.cds.caltech.edu/~utopcu/index.php/Short_Course:_Quantitative_Local_Analysis_of_Nonlinear_Systems_Using_Sum-of-Squares_Decompositions Material on part III]. Links to software packages, slides, and notes on quantitative analysis of nonlinear systems. Shorter version is in these [http://www.cds.caltech.edu/~utopcu/cdc10vvslides/UfukTopcu.pdf slides]
* [http://etd.caltech.edu/etd/available/etd-05272005-144358/ Stephen Prajna's dissertation] on verifying temporal properties for hybrid dynamical systems. 
* [http://www.cds.caltech.edu/~utopcu/images//9/9b/TPSB-CSM-2010.pdf Help on SOS]: a paper on the very basics of sum-of-squares programming and their use in nonlinear system verification.
* [http://arxiv.org/abs/math.OC/0103170 Minimizing Polynomial Functions] by P. Parrilo and B. Sturmfels on global optimization of polynomial functions and Positivstellensatz (generalizations of the S-procedure). 
* [http://robotics.eecs.berkeley.edu/~sastry/ee291e/lygeros.pdf Lecture Notes on Hybrid Systems] (by John Lygeros): A rough introduction to hybrid systems. Chapters 5 and 6 are on various analysis techniques relevant for this short course.

EECI 2012: Temporal Logic

2012-05-13T15:38:38Z

Utopcu:

{{AFRL12 header|prev=Automata Theory|next=Model Checking}}
{{righttoc}}

In this lecture we introduce ''linear temporal logic'' (LTL), a mathematical language for describing linear time properties of transition systems. After a short introduction to the concept of temporal logics, we introduce the syntax and semantics of LTL, including examples. Examples of LTL specifications for control protocols are drawn from the applications given in the introductory lecture. If time permits, we will also briefly introduce other temporal logics and describe some of the differences between various formulations.

== Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/EECI2012/L2_ltl_14May12.pdf Linear Temporal Logic] (Presentation and notation follow that in "Principles of Model Checking" chapter 5.1 by Baier and Katoen.)

== Further Reading ==
* [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://research.microsoft.com/en-us/um/people/lamport/tla/book.html ''Specifying Systems''], L. Lamport.. Addison-Wesley, 2002. This is a very readable text on specification using temporal logic of actions (LTA).

== Additional Information ==
* [http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/ LTL2BA] - a web page (and program) for converting LTL formulas to Buchi automata.

EECI 2012: Receding Horizon Temporal Logic Planning

2012-04-22T06:13:11Z

Utopcu:

{{AFRL12 header|prev=Synthesis of Reactive Control Protocols |next=TuLiP}}

This lecture introduces the receding horizon temporal logic planning. Introductory material on high computational complexity of reactive control protocol synthesis is followed by the statement and discussion of a main result and a small example. We discuss implementation details, further extensions, and a hierarchical control structure that utilizes the proposed receding horizon temporal logic planning procedure. At the end, we discuss an abstraction procedure based on finite-time reachability from control theory for constructing finite-state approximations of the underlying continuous dynamics.

{{righttoc}}

== Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/AFRL2012/L8_RHTLP.pdf Receding Horizon Temporal Logic Planning]

== Further Reading and Additional Information ==
* [http://www.cds.caltech.edu/~utopcu/images//4/4d/WTM-itac10R.pdf Receding horizon temporal logic planning],T. Wongpiromsarn, U. Topcu, and R. Murray, submitted to IEEE Transactions on Automatic Control, 2010. Details on the receding horizon temporal logic planning. 
* [http://www.cds.caltech.edu/~murray/wiki/index.php/EECI08:_Optimization-Based_Control Optimization based control]. A page prepared for EECI 2008 with information and material on basic receding horizon control.
* [http://control.ee.ethz.ch/~mpt/ Multiparametric Toolbox] The Multi-Parametric Toolbox (MPT) is a free Matlab toolbox for design, analysis and deployment of optimal controllers for constrained linear, nonlinear and hybrid systems. [http://www.cds.caltech.edu/tulip The receding horizon temporal logic planning toolbox] uses the polytope manipulation (intersection, union, set difference, projection, etc.) functionalities of MPT. 

* [http://www.cds.caltech.edu/~utopcu/images//9/98/WTM-aaai10.pdf Automatic synthesis of robust embedded control software], T. Wongpiromsarn, U. Topcu, and R. Murray, AAAI 2010 Spring Symposium on Embedded Reasoning: Intelligence in Embedded Systems, 2010. Details on the abstraction procedure covered in this lecture. 

* [http://www.mpc.berkeley.edu/mpc-course-material/BBMbook_Cambridge.pdf?attredirects=0&d=1 Predictive Control]: A book draft by Bemporap, Borrelli, and Morari. Details on some of the ideas in the implementation of the abstraction procedure presented in the slides can be found in this book.

EECI 2012: Receding Horizon Temporal Logic Planning

2012-04-22T06:13:00Z

Utopcu: Created page with '{{AFRL header|prev=Synthesis of Reactive Control Protocols |next=TuLiP}} This lecture introduces the receding horizon temporal logic planning. Introductory material on high co…'

{{AFRL header|prev=Synthesis of Reactive Control Protocols |next=TuLiP}}

This lecture introduces the receding horizon temporal logic planning. Introductory material on high computational complexity of reactive control protocol synthesis is followed by the statement and discussion of a main result and a small example. We discuss implementation details, further extensions, and a hierarchical control structure that utilizes the proposed receding horizon temporal logic planning procedure. At the end, we discuss an abstraction procedure based on finite-time reachability from control theory for constructing finite-state approximations of the underlying continuous dynamics.

{{righttoc}}

== Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/AFRL2012/L8_RHTLP.pdf Receding Horizon Temporal Logic Planning]

== Further Reading and Additional Information ==
* [http://www.cds.caltech.edu/~utopcu/images//4/4d/WTM-itac10R.pdf Receding horizon temporal logic planning],T. Wongpiromsarn, U. Topcu, and R. Murray, submitted to IEEE Transactions on Automatic Control, 2010. Details on the receding horizon temporal logic planning. 
* [http://www.cds.caltech.edu/~murray/wiki/index.php/EECI08:_Optimization-Based_Control Optimization based control]. A page prepared for EECI 2008 with information and material on basic receding horizon control.
* [http://control.ee.ethz.ch/~mpt/ Multiparametric Toolbox] The Multi-Parametric Toolbox (MPT) is a free Matlab toolbox for design, analysis and deployment of optimal controllers for constrained linear, nonlinear and hybrid systems. [http://www.cds.caltech.edu/tulip The receding horizon temporal logic planning toolbox] uses the polytope manipulation (intersection, union, set difference, projection, etc.) functionalities of MPT. 

* [http://www.cds.caltech.edu/~utopcu/images//9/98/WTM-aaai10.pdf Automatic synthesis of robust embedded control software], T. Wongpiromsarn, U. Topcu, and R. Murray, AAAI 2010 Spring Symposium on Embedded Reasoning: Intelligence in Embedded Systems, 2010. Details on the abstraction procedure covered in this lecture. 

* [http://www.mpc.berkeley.edu/mpc-course-material/BBMbook_Cambridge.pdf?attredirects=0&d=1 Predictive Control]: A book draft by Bemporap, Borrelli, and Morari. Details on some of the ideas in the implementation of the abstraction procedure presented in the slides can be found in this book.

EECI 2012: Computer Session: TuLiP

2012-04-22T03:48:56Z

Utopcu:

{{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://www.cds.caltech.edu/~utopcu/AFRL2012/C2_TuLiP.pdf TuLiP] (Exercises are at the end of the slides.)

== 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: Computer Session: TuLiP

2012-04-22T03:48:26Z

Utopcu:

{{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://www.cds.caltech.edu/~utopcu/AFRL2012/C2_TuLiP.pdf TuLiP]

== 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: Computer Session: TuLiP

2012-04-22T03:40:11Z

Utopcu: /* Additional Information */

{{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://www.cds.caltech.edu/~utopcu/AFRL2012/L11_tulip-24Mar11.pdf TuLiP]

== 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: Computer Session: TuLiP

2012-04-22T03:39:10Z

Utopcu: /* Additional Information */

{{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://www.cds.caltech.edu/~utopcu/AFRL2012/L11_tulip-24Mar11.pdf TuLiP]

== 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] 
* [https://www.cds.caltech.edu/subversion/nok/rhtlp/trunk/doc/build/html/index.html TuLiP Documentation] For guest access, use ''anonymous'' as username with no password 
* [http://jtlv.ysaar.net/ JTLV Project Home Site] JTLV provides the framework for the underlying digital design synthesis routine used in TuLiP.

EECI 2012: Computer Session: TuLiP

2012-04-22T03:38:34Z

Utopcu:

{{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://www.cds.caltech.edu/~utopcu/AFRL2012/L11_tulip-24Mar11.pdf TuLiP]

== 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://www.cds.caltech.edu/tulip/ TuLiP] 
* [https://www.cds.caltech.edu/subversion/nok/rhtlp/trunk/doc/build/html/index.html TuLiP Documentation] For guest access, use ''anonymous'' as username with no password 
* [http://jtlv.ysaar.net/ JTLV Project Home Site] JTLV provides the framework for the underlying digital design synthesis routine used in TuLiP.

EECI 2012: Computer Session: TuLiP

2012-04-22T03:37:58Z

Utopcu: Created page with '{{AFRL header|prev=Receding Horizon Temporal Logic Planning |next=....}} This lecture provides an overview of TuLiP, a Python-based software toolbox for the synthesis of embedde…'

{{AFRL 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://www.cds.caltech.edu/~utopcu/AFRL2012/L11_tulip-24Mar11.pdf TuLiP]

== 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://www.cds.caltech.edu/tulip/ TuLiP] 
* [https://www.cds.caltech.edu/subversion/nok/rhtlp/trunk/doc/build/html/index.html TuLiP Documentation] For guest access, use ''anonymous'' as username with no password 
* [http://jtlv.ysaar.net/ JTLV Project Home Site] JTLV provides the framework for the underlying digital design synthesis routine used in TuLiP.

EECI 2012: Automata Theory

2012-04-22T03:08:54Z

Utopcu:

{{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.21, 3.2-3.5, and 4.1-4.3 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-04-22T03:06:04Z

Utopcu:

{{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/eeci2011/L2_Automata_Theory.pdf Automata Theory] (presentation and notation follow that in "Principles of Model Checking" chapters 2.1, 2.21, 3.2-3.5, and 4.1-4.3 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-04-22T03:04:55Z

Utopcu: Created page with '{{eeci-sp11 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 t…'

{{eeci-sp11 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/eeci2011/L2_Automata_Theory.pdf Automata Theory] (presentation and notation follow that in "Principles of Model Checking" chapters 2.1, 2.21, 3.2-3.5, and 4.1-4.3 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: Hybrid Systems Verification

2012-04-22T03:02:55Z

Utopcu:

{{AFRL12 header|prev=... |next=...}}

This lecture focuses on the verification of hybrid systems. We first discuss finite-state under- and over-approximations of hybrid dynamics and how these finite-state models coupled with the model checking tools can be used to verify temporal logic properties against hybrid dynamics. Then, we move to deductive verification and a computational procedure for constructing Lyapunov-type functions (e.g., barrier certificates) which witness the fact that a hybrid system satisfies certain temporal specifications. We finally introduce the notions of approximate bisimulations and bisimulation functions and how they can be used in verification of temporal properties.

{{righttoc}}

== Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/AFRL2012/L6_Hybrid_Systems_Verification.pdf Hybrid Systems Verification]

== Additional Material and Further Reading ==
* [http://www.cds.caltech.edu/~utopcu/index.php/Short_Course:_Quantitative_Local_Analysis_of_Nonlinear_Systems_Using_Sum-of-Squares_Decompositions Material on part III]. Links to software packages, slides, and notes on quantitative analysis of nonlinear systems. Shorter version is in these [http://www.cds.caltech.edu/~utopcu/cdc10vvslides/UfukTopcu.pdf slides]
* [http://etd.caltech.edu/etd/available/etd-05272005-144358/ Stephen Prajna's dissertation] on verifying temporal properties for hybrid dynamical systems. 
* [http://www.cds.caltech.edu/~utopcu/images//9/9b/TPSB-CSM-2010.pdf Help on SOS]: a paper on the very basics of sum-of-squares programming and their use in nonlinear system verification.
* [http://arxiv.org/abs/math.OC/0103170 Minimizing Polynomial Functions] by P. Parrilo and B. Sturmfels on global optimization of polynomial functions and Positivstellensatz (generalizations of the S-procedure). 
* [http://robotics.eecs.berkeley.edu/~sastry/ee291e/lygeros.pdf Lecture Notes on Hybrid Systems] (by John Lygeros): A rough introduction to hybrid systems. Chapters 5 and 6 are on various analysis techniques relevant for this short course.

EECI 2012: Hybrid Systems Verification

2012-04-22T02:55:06Z

Utopcu: Created page with '{{eeci-sp11 header|prev=Computer Lab I |next=Autonomous Driving}} This lecture focuses on the computational verification of temporal specifications for hybrid, nonlinear dynamic…'

{{eeci-sp11 header|prev=Computer Lab I |next=Autonomous Driving}}

This lecture focuses on the computational verification of temporal specifications for hybrid, nonlinear dynamical systems and associated software packages. We discuss a procedure for computing algebraic functions (e.g., Lyapunov, storage, barrier functions) that witness the fact that a dynamical system satisfies certain temporal specifications. We discuss applications of this procedure to stability, input-output gain, safety, and eventuality verification. The notion of approximate bisimulations is introduced and use of so-called bisimulation functions in temporal property verification is discussed.

{{righttoc}}

== Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/AFRL2012/L6_Hybrid_Systems_Verification.pdf Hybrid Systems Verification]

== Additional Material and Further Reading ==
* [http://www.cds.caltech.edu/~utopcu/index.php/Short_Course:_Quantitative_Local_Analysis_of_Nonlinear_Systems_Using_Sum-of-Squares_Decompositions Material on part III]. Links to software packages, slides, and notes on quantitative analysis of nonlinear systems. Shorter version is in these [http://www.cds.caltech.edu/~utopcu/cdc10vvslides/UfukTopcu.pdf slides]
* [http://etd.caltech.edu/etd/available/etd-05272005-144358/ Stephen Prajna's dissertation] on verifying temporal properties for hybrid dynamical systems. 
* [http://www.cds.caltech.edu/~utopcu/images//9/9b/TPSB-CSM-2010.pdf Help on SOS]: a paper on the very basics of sum-of-squares programming and their use in nonlinear system verification.
* [http://arxiv.org/abs/math.OC/0103170 Minimizing Polynomial Functions] by P. Parrilo and B. Sturmfels on global optimization of polynomial functions and Positivstellensatz (generalizations of the S-procedure). 
* [http://robotics.eecs.berkeley.edu/~sastry/ee291e/lygeros.pdf Lecture Notes on Hybrid Systems] (by John Lygeros): A rough introduction to hybrid systems. Chapters 5 and 6 are on various analysis techniques relevant for this short course.

EECI 2012: Model Checking and Logic Synthesis

2012-04-22T02:30:34Z

Utopcu: /* Further Reading */

{{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://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.)

== 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: Model Checking and Logic Synthesis

2012-04-22T00:40:54Z

Utopcu:

{{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://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.)

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

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

EECI 2012: Model Checking and Logic Synthesis

2012-04-22T00:40:09Z

Utopcu:

{{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://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.)

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

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

EECI 2012: Model Checking and Logic Synthesis

2012-04-22T00:39:48Z

Utopcu:

{{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://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.)

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

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

EECI 2012: Model Checking and Logic Synthesis

2012-04-22T00:39:28Z

Utopcu:

{{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://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.)

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

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

EECI 2012: Model Checking and Logic Synthesis

2012-04-22T00:38:20Z

Utopcu:

{{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 XXX) and discuss the computational complexity of model checking.

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

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

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

Template:AFRL12 header

2012-04-22T00:36:51Z

Utopcu: Created page with 'Return to Caltech/AFRL 2012 Main Page'

[[Caltech/AFRL,_Spring_2012|Return to Caltech/AFRL 2012 Main Page]]

EECI 2012: Model Checking and Logic Synthesis

2012-04-22T00:34:03Z

Utopcu:

{{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 XXX) and discuss the computational complexity of model checking.

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

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

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

EECI 2012: Model Checking and Logic Synthesis

2012-04-22T00:29:21Z

Utopcu:

{{righttoc}}

This lecture provides an introduction to automata based model checking. We first describe how automata based model checking works, including an efficient algorithm for computing language intersection. The rest of the lecture focuses on the use of Spin model checker and the computational complexity issue.

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

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

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