HYBRID SYSTEMS

PDEEC

Spring 2010

Course description

This class is about models, analysis and design of hybrid systems.

The rich and exciting research over the past decade concerning the description, analysis, controller design, simulation, and implementation of hybrid systems is presented in a coherent fashion.

From control engineering, this research has inherited the concepts and theories of optimality, stability, controlled differential equation models, and the motivation to improve the performance of increasingly complex physical processes. From computer science, the research has incorporated the theories of logical specification and verification, event-driven state machine models, concurrent processes and object-oriented approaches.

There is an equal emphasis on the conceptual and theoretical contributions and on tools and techniques that yield more immediately practical benefits.

Contents of this page

Late breaking news
Administrative
Prerequisites
Assessment format
Projects
Detailed syllabus
Homeworks
Related courses and links
Computational tools

o Modelling, analysis and simulation

o Reach set computation

o Level set methods

o Model checking and verification tools

References

o Textbooks

o Papers

§ Modelling

§ Reachability and verification

§ Algorithmic analysis of hybrid systems

§ Control design

§ Applications

· Related links

· How to write a paper

· To probe further

Late breaking news

Deadline for the delivery of Homework #5 was postponed until May 6th.
Randy Beard from BYU will give an invited lecture May 27^th.

Administrative

Instructors:

João Borges de Sousa, E-mail: jtasso @ fe.up.pt; Office I215; Tel: 22 508 1690

Fernando Lobo Pereira, E-mail: flp @ fe.up.pt; Office I218, Tel: 22 508 1857

Office Hours: by appointment

Prerequisites

Consent of the instructors is required.

This course is open to PDEEC, MAPI and ECE students.

Recommended preparation: The students should be familiar with linear algebra and basic control systems and some programming language.

Assessment format

Homeworks – 50% (9-10 assignments)

Final Project – 50% (paper and presentation at the end of the semester)

Projects

What is the project?

q Independent/individual research project on a topic selected from the list of projects suggested by the instructors (other topics may be discussed and accepted).

List of projects

Choosing a project: An e-mail with the selection is due April 5^th

Detailed syllabus

This is a work in progress. Comments and suggestions are welcome. Please send them to [email protected]

Class	Content	Lecture notes	Required readings	Optional readings
Lec #1 22-02-10	Course outline Assessment format Class projects Introduction to hybrid systems q Examples q Aspects of hybrid systems behaviour Formal models q Automata q Ordinary differential equations q Hybrid automata q Stochastic hybrid automata Existence and uniqueness		Hybrid and Switched Systems ECE229 — Fall 2005, João Hespanha Lecture 1 Lecture 2 Lecture 3
Lec #2 23-02-10	Background on continuous-time systems q Reach sets q Invariance Signals and systems Descriptions of systems System’ specifications for state-space models	Lecture notes Notes on reachability	[1] chapters 1, 2, 3, 4, 6
Lec #3 04-03-10	Background on continuous-time systems q Reach set computation q Invariance q Optimal control and reach sets Simulation of hybrid systems	Lecture notes Notes on reachability StateFlow tutorial	Hybrid and Switched Systems ECE229 — Fall 2005, João Hespanha Lecture 4	[17]
Lec #4 11-03-10	Simulation of hybrid systems Examples	Examples
Lec #5 18-03-10	Properties of hybrid systems q Sequence q Safety q Liveness Formal specification Decidability Model checking and verification Reachability q Transition systems q Reachability algorithms q Controller synthesis based on reachability		Hybrid and Switched Systems ECE229 — Fall 2005, João Hespanha Lecture 5 Hybrid and Switched Systems ECE229 — Fall 2005, João Hespanha Lecture 6	[24-32]
Lec #6 25-03-10	Reachability and optimal control q Motivation. q Optimal control problem formulation.	Lecture notes on optimal control		[18-23]
Lec #7 08-04-10	Reachability and optimal control q Necessary Conditions of Optimality - Linear Systems q Linear Systems Without and with state constraints.
Lec #8 15-04-10	Reachability and optimal control q Linear Systems Without and with state constraints. Minimum time. Linear quadratic regulator. q The maximum principle and reachability
Lec #9 22-04-10	Formal models of hybrid systems Dynamic networks of hybrid automata Models of systems with evolving structure SHIFT language	Lecture notes on DNHA SHIFT (see web page below)	[2] [33]
Lec #10 22-04-10	Models of systems with evolving structure Formal models of control architectures SHIFT language	Lecture notes on coordination and control of networked vehicle systems	[42] [46]
Lec #11 29-04-10	The Ellipsoidal Toolbox (see web page below)
Lec #12 13-05-10	Stability	Lecture notes	Hybrid and Switched Systems ECE229 — Fall 2005, João Hespanha Lecture 7	Sontag’s book
Lec #13 20-05-10	Stability of hybrid systems		Hybrid and Switched Systems ECE229 — Fall 2005, João Hespanha Lecture 8 Notes on stability of hybrid systems by M. Branicky Notes on stability of hybrid systems by C. Tomlin
	Optimization and level set methods	The Level sets Toolbox (see web page below)
	Background on continuous-time systems q Optimal control techniques for reach set computation q Constructive method for solving a class of differential games	Lecture notes	[2], [5]	[2-17]
Lec #11 TBD	Optimal control of hybrid systems
Lec #12 TBD 09
Lec #13 TBD
Lec #14 TBD	Control architectures
Student project presentations
Lec #15	Presentations			Supplemental notes: UPPAAL Model Checker Overview Presented by Valério Rosset. Crash course on model checking by Stavros Tripakis [32]

Homeworks

#	Description	Due date
PART I Concepts and interpretation of control systems
HW #1	Reading assignment q Chapters 1, 2 and 3 of [1] Quiz#1	01-03-10
HW #2	Reading assignment q Chapter 4 of [1] Quiz#2 Homework#2	11-03-10
HW #3	Exercises 1-17 from Lecture notes	18-03-10
HW #4	Homework#4	22-03-10
HW #5	Exercises 18-23 from Lecture notes Homework#5	8-04-10 06-05-10
HW #5	Project proposals due: what,why and how.	05-04-10
HW #6	State-flow programs Run the examples from the class and present the conclusions	21-04-09
HW #7	Ellipsoidal toolbox and reachability	25-05-09
HW #8	SHIFT Programming	01-06-09
HW #9	Level sets toolbox	08-06-09

Related courses

Ed Lee and Pravin Varaiya http://ptolemy.eecs.berkeley.edu/eecs20/

João Hespanha http://www.ece.ucsb.edu/~hespanha/ece229/

Karl Henrik Johansson http://www.s3.kth.se/control/kurser/2E1245/

J. Lygeros Lecture Notes on Hybrid Systems, Notes for an ENSIETA short course, Feb 2004.

J. Lygeros, C. Tomlin and S. Sastry Art of Hybrid Systems, Compendium of Lecture Notes for the Hybrid Systems Class, 2002.

Maria Prandini http://home.dei.polimi.it/prandini/sistemi-ibridi.htm

T. John Koo http://www.vuse.vanderbilt.edu/~kootj/Class/2004/Spring/index.html

Computational tools

Modeling, analysis and simulation

SHIFT, Hybrid systems simulation language, http://path.berkeley.edu/shift/

PC-SHIFT, http://path.berkeley.edu/~vjoel/pcshift/

Simulink/State Flow, http://www.mathworks.com/products/stateflow/

Omola, http://www.control.lth.se/~cace/omsim.html

TrueTime, Simulation of networked and embedded control systems, http://www.control.lth.se/truetime/

Ptolemy II, Modelling, simulation, and design of concurrent, real-time, embedded systems, http://ptolemy.eecs.berkeley.edu/

HyTech, Automatic tool for the analysis of embedded systems, http://embedded.eecs.berkeley.edu/research/hytech/

HyVisual, Hybrid System Visual Modeler, http://ptolemy.eecs.berkeley.edu/ptolemyII/hyvisual2.2/index.htm

Charon, Modular Specification of Hybrid Systems, http://rtg.cis.upenn.edu/mobies/charon/CHARONpapers.html

Reach set computation

Ellipsoidal Toolbox (ET), Alex A. Kurzhanskiy, http://www.eecs.berkeley.edu/~akurzhan/ellipsoids/

d/dt Reachability Analysis of Continuous and Hybrid Systems, http://www-verimag.imag.fr/~tdang/ddt.html

Level set methods

A Toolbox of Level Set Methods, version 1.1, Ian Mitchell – http://www.cs.ubc.ca/~mitchell/ToolboxLS/index.html

Interactive demonstrations of Fast Marching, http://math.berkeley.edu/~sethian/2006/Applets/Menu_Expanded_Applets.html

Model checking and verification tools

Kronos, http://www-verimag.imag.fr/TEMPORISE/kronos-english.html

Checkmate, Hybrid System Verification Toolbox for Matlab, http://www.ece.cmu.edu/~webk/checkmate/

UPPAAL, http://www.uppaal.com/

SPIN, http://spinroot.com/spin/whatispin.html

References

Students are encouraged to look into the proceedings of:

Hybrid Systems: Computation and Control workshop.
Control and Decision Conference
American Control Conference
European Control Conference
IFAC World Conference
International Conference on Robot Communication and Coordination

Textbooks

[1] Edward A. Lee and Pravin Varaiya,. Structure and Interpretation of Signals and Systems. Springer-Verlag, 2000.

Papers

Modeling

[2] T. Simsek, J. Borges de Sousa and P. Varaiya, "Communication and control in hybrid systems", Tutorial session, Proceedings of the American Control Conference, Washington, US, July 2001.

[3] P. J. Mosterman An Overview of Hybrid Simulation Phenomena and their support by simulation packages, in HYbrid Systems: COmputation and COntrol, W. VaanDrager and J. van Schuppen (editors), Springer Verlag Lectures Notes in Computer Science, Vol. LNCS-1569, 1999, pp. 178-192.

[4] Luca Carloni, Maria D. Di Benedetto, Alessandro Pinto and Alberto Sangiovanni-Vincentelli Modeling Techniques, Programming Languages Design Toolsets and Interchange Formats for Hybrid Systems EU-IST Columbus Project, DHS3 Report, 2004.

[5] Kim G. Larsen, B. Steen and C. Weise, Continuous modelling of real-time and hybrid systems: from concepts to tools, International Journal on Software Tools for Technology Transfer (1997) 1: 64-85.

[6] Jun Zhang, K. Johansson, John Lygeros, S. Sastry. Dynamical Systems Revisited: Hybrid Systems with Zeno Executions. In Nancy A. Lynch and Bruce H. Krogh (ed.). Hybrid Systems: Computation and Control. Springer, Mar. 2000.

[7] M. S. Branicky, V. S. Borkar, and S. K. Mitter. A unified framework for hybrid control: model and optimal control theory. IEEE Transactions on Automatic Control, 43(1):31--45, 1998.

[8] M. S. Branicky. Studies in Hybrid Systems: Modeling, Analysis and Control. PhD thesis, MIT, 1995.

[9] R. W. Brockett. Dynamical systems and their associated automata. In R. Menicken U. Helmke and J. Saurer (editors). Mathematical Theory and Applications, pages 29--57. Akademie Verlag, 1994.

[10] H. Witsenhausen. A class of hybrid-state continuous-time dynamic systems. IEEE Transactions on Automatic Control, 11(2):161--167, 1966.

[11] Jean-Pierre Aubin. mpulse differential equations and hybrid systems: A viability approach. Lecture Notes, University of California at Berkeley, 2000.

[12] E. Lee and A. Sangiovanni-Vincentelli. Comparing models of computation, http://ptolemy.eecs.berkeley.edu/~eal/talks/index.html. 1996.

[13] Z. Manna O. D. Maler and A. Pnueli. From timed to hybrid systems. In W. Roever J. Bakker, K. Huizing and G. Rozenberg (editors). Real-Time: Theory in Practice, LNCS 600, pages 447--484. Springer-Verlag, 1992.

[14] G. Pappas. Hybrid Systems: Computation and Abstraction. PhD thesis, University of California at Berkeley, 1998.

[15] Anuj Puri. Theory of hybrid systems and discrete event systems. PhD thesis, University of California at Berkeley, 1995.

[16] J. Borges de Sousa and F. Lobo Pereira. Some questions about hybrid systems. Proceedings of the European Control Conference, 2001.

[17] Robin Milner. Semantic ideas in computing. In Ian Wand and Robin Milner (editors). Computing tomorrow : future research directions in computer science}, pages 246--283. Cambridge University Press, 1996.

Reachability and verification

[18] P. Varaiya. Reach set computation using optimal control. Proceedings of the KIT Workshop on Verification of Hybrid Systems. Verimag, Grenoble, France, 1998.

[19] A. B. Kurzhanskii and P. Varaiya. Ellipsoidal techniques for reachability analysis. In N. Lynch and B. Krogh (editors). Computation and control, Lecture Notes in Computer Science, pages 202--214. Springer-Verlag, 2000.

[20] A. B. Kurzhanskii and P. Varaiya. On reachability under uncertainty. Siam Journal of Control and Optimization, 2001.

[21] B. H. Krogh and O. Stursberg, On efficient representation and computation of reachable sets for hybrid systems, in Hybrid Systems: Computation and Control (HSCC'03), Lecture Notes in Computer Science (LNCS), Springer.

[22] M. Broucke. A geometric approach to bisimulation and verification of hybrid systems. Proceedings of the 37th IEEE Conference on Decision and Control Conference, pages 4277--82. IEEE, 1998.

[23] B. H. Krogh and O. Stursberg, On efficient representation and computation of reachable sets for hybrid systems, in Hybrid Systems: Computation and Control (HSCC'03), Lecture Notes in Computer Science (LNCS), Springer..

Algorithmic analysis of hybrid systems

[24] R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138(1), 1995.

[25] R. Alur and T.A. Henzinger. A really temporal logic. Proceedings of the 30th Annual Symposium on Foundations of Computer Science, pages 164--169. IEEE Computer Society Press, 1989.

[26] R. Alur and T.A. Henzinger. Real-time logics: complexity and expressiveness. Proceedings of the Fifth Annual Symposium on Logic in Computer Science, pages 390--401. IEEE Computer Society Press, 1990.

[27] R. Alur, T.A. Henzinger and O. Kupferman. Alternating-time temporal logic. Proceedings of the 38th Annual Symposium on Foundations of Computer Science, pages 100--109. IEEE Computer Society Press, 1997.

[28] T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193--244, 1994.

[29] T.A. Henzinger, B. Horowitz, and R. Majumdar. Rectangular hybrid games. In J.C.M. Baeten and S.~Mauw, (editors). CONCUR 99: Concurrency Theory, Lecture Notes in Computer Science 1664, pages 320--335. Springer-Verlag, 1999.

[30] R. P. Kurshan. Computer-aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, 1994.

[31] S. Yovine. Methods et Outils pour la Verification Symbolique de Systemes Temporises. PhD thesis, Institut National Polytechnique de Grenoble -- France, 1993.

[32] Thomas A. Henzinger, The Symbolic Approach to Hybrid Systems, (CAV '02), UC Berkeley,

Control design

[33] C. Tomlin, I. Mitchell, A. Bayen, and M. Oishi, Computational Techniques for the Verification and Control of Hybrid Systems, Proceedings of the IEEE, Volume 91, Number 7, July 2003.

[34] Claire Tomlin, John Lygeros, and Shankar Sastry, A Game Theoretic Approach to Controller Design for Hybrid Systems, Proceedings of the IEEE, Volume 88, Number 7, July 2000.

[35] J. Borges de Sousa, K. H. Johansson, J. Silva and Alberto Speranzon, “A verified hierarchical control architecture for coordinated multi-vehicle operations”, International Journal of Adaptive Control and Signal Processing, International Journal of Adaptive Control and Signal Processing, Volume 21, Issue 2-3, Pages 159 – 188 (Special Issue: Autonomous and adaptive control of vehicles in formation . Issue Edited by Sandor M. Veres).

[36] P. Varaiya. Control design of an automated highway system. Proceedings of the IEEE, 88(7):913--25, July 2000.

[37] A. Deshpande and P. Varaiya. Viable control of hybrid systems. Hybrid Systems II, pages 128--147. Springer, 1995.

[38] J. Lygeros, D.N. Godbole, and S. Sastry. Verified hybrid controllers for automated vehicles. IEEE Transactions on Automatic Control, 43(4):522--39, April 1998.

[39] Paulo Tabuada and George J. Pappas, Linear temporal logic control of linear systems, IEEE Transactions on Automatic Control, Submitted February 2004.

[40] T. J. Koo, S. Sastry, Bisimulation Based Hierarchical System Architecture for Single-Agent Multi-Modal Systems, Hybrid Systems: Computation and Control, Lecture Notes in Computer Science, Vol. 2289, pp. 281-293, Springer-Verlag, 2002.

Applications

[41] A. Antoniotti, A. Desphande, and A. Girault. Microsimulation analysis of multiple merge junctions under autonomous ahs operation. Proceedings of Conference on Intelligent Transportation Systems ITSC '97}, pages 147--52. IEEE, 1997.

[42] J. Borges de Sousa, A. Girard, and K. Hedrick. Real-time hybrid control of mobile offshore base scaled models. Proceedings of the American Control Conference, 2000.

[43] D. Godbole, N. Kourjanskaia, R. Sengupta, and M. Zandonadi. Methodology for an adaptive cruise control study using the shift/smart-ahs framework. Proceedings of 1998 IEEE International Conference on Systems, Man, and Cybernetics, pages 3217--22. IEEE, 1998.

[44] A. Gollu and P. Varaiya. Smartahs: a simulation framework for automated vehicles and highway systems. Mathematical and Computer Modeling, 27(9-11):103--28, 1998.

[45] P. Varaiya. Smart cars on smart roads: problems of control. IEEE Transactions on Automatic Control}, 38(3):195--207, February 1993.

[46] J. Borges de Sousa, T. Simsek e P. Varaiya, “Task planning and execution for UAV teams”, Proceedings of the Decision and Control Conference, Bahamas, 2004.

How to write a paper

There are lots of references on writing a paper on the web. The following are recommended:

· J. Hespanha. Writing a Control Paper. Sep. 2006. Unpublished.

· Simon Peyton Jones. How to write a great research paper. Microsoft research.

To probe further

We have witnessed over the last decade impressive advancements in computation, control, communication, sensing, vehicle, and system design. Despite the advances in all these areas and, in particular in hybrid systems, we are still far from being able to design and deploy networked vehicles and systems in a systematic manner and within an appropriate scientific framework.

The common denominator of all the applications of networked vehicles and systems is the concept of system of systems. In all applications there are in fact several systems interacting: software components, physical devices, such as sensors and robotic vehicles, and human operators. The system resulting from these interactions possesses new properties, different from those of each single component. Some of these properties are as planned, whereas others are emergent and eventually lead to unpredictable behaviors.

The design and deployment of networked vehicles and systems in a systematic manner and within an appropriate scientific framework requires a significant expansion of the basic tool sets from different areas (computation, control, communication, sensing and vehicle design) and the introduction of fundamentally new techniques that extend and complement the existing state of the art. Furthermore, these advances can only be achieved by adopting an inherently interdisciplinary approach, bringing together researchers from traditionally separate communities disseminated all over the world to work on problems at the forefront of science and technology.

At the Underwater Systems and Technologies Laboratory at Porto University we have been developing state of the art tools and technologies for network vehicle systems in cooperation researchers with the University of California at Berkeley, the Naval Postgraduate School, the University of Michigan and with the Royal Institute of Technology in Stockholm.

Last update: 16-04-2010