EECE 396-1

Hybrid and Embedded Systems: Computation

T. John Koo

300 Featheringill Hall
Tu/Th 11:00am-12:30pm
 

The multi-disciplinary research field of hybrid systems has emerged over the last decade and lies at the boundaries of computer science, control engineering and applied mathematics. In general, a hybrid system can be defined as a system built from atomic discrete components and continuous components by parallel and/or serial composition, arbitrarily nested. The behaviors and interactions of components are governed by models of computation.

The hybrid phenomena captured by such mathematical models are manifested in a great diversity of complex engineering applications such as real-time systems, embedded software, robotics, mechatronics, aeronautics, and process control. The high-profile and safety-critical nature of such applications has fostered a large and growing body of work on formal methods for hybrid systems: mathematical logic, computational models and methods and automated reasoning tools supporting the formal specification and verification of performance requirements for hybrid systems, and the design and synthesis of control programs for hybrid systems that are provably correct with respect to formal specifications.

This course investigates modeling, analysis and verification of various classes of hybrid systems.  Special attention  is paid to computational and simulation tools for hybrid systems. Applications ranging from networked sensors, power electronics, avionics, autonomous vehicles will be covered.  The course consists of lectures, a handful of homeworks, and a final project.

Information

Office: 376 Jacobs Hall

Office Hours: Tuesday 2:00pm-3:00pm

Email: john.koo@vanderbilt.edu

URL: http://www.vuse.vanderbilt.edu/~kootj

Grading

Homework

Homework captures both theory and applications.

Reading

Weekly reading will be assigned.

Project

Potential project topics will be announced during the course.

Prerequisites

Students should understand basic concepts in differential equations, dynamical systems and logic. They should know how to program in some language; for example, Matlab, Mathematica, Java or C. Familiarity with control theory and/or automata theory may be useful.

Recommended Texts

R. Alur, T.A. Henzinger, H. Wong-Toi. Symbolic analysis of hybrid systems. Proceedings of the 37th IEEE Conference on Decision and Control, Invited survey, 1997.

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

E. Asarin, O. Bournez, T. Dang, O. Maler, and A. Pnueli, Effective Synthesis of Switching Controllers for Linear Systems,
In Proceedings of the IEEE, 88, Special Issue Hybrid System: Theory & Applications, 1011-1025, 2000.

Thao Dang, Alexandre Donze, and Oded Maler, Verification of Analog and Mixed-Signal Circuits using Hybrid Systems Techniques, Submitted to DAC'04 - Design Automation Conference, June 2004.

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

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

Gerardo Lafferriere, George J. Pappas, and Sergio Yovine, Symbolic reachability computations for families of linear vector fields,  Journal of Symbolic Computation, 32(3):231-253, September 2001.

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.

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.

Matthew Senesky, Gabriel Eirea, and T. John Koo, Hybrid Modelling and Control of Power Electronics, Hybrid Systems: Computation and Control April,  Lecture Notes in Computer Science, Vol. 2623, pp. 450-465, Springer-Verlag, 2003.

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.

Class Schedule

January 15	Introduction
January 20	Examples: Hybrid Automata	Slides (updated on 1/22/04)
January 22	Modeling: Finite State Machine	Slides (updated on 1/22/04) HW1 (updated on 1/22/04)
January 27	No Class
January 29	Modeling: Time Automata Tool: HyTech	Slides (updated on 1/29/04)
February 3	Modeling: Ordinary Differential Equations Tool: Matlab	Slides (updated on 2/03/04)
February 5	Modeling: Hybrid Automata Tool: HyVisual	Slides (updated on 2/05/04)
February 10	Analysis: Reachability - Discrete	Slides (updated on 2/10/04)
February 12	Analysis: Reachability - Continuous	Slides (updated on 2/12/04)
February 17	Analysis: Reachability - Hybrid	Slides (updated on 2/17/04)
February 19	Analysis: Reachability - Hybrid Tool: Requiem
February 24	Tool: Ptolemy II - Multi-Modal Systems Guest: Eric Manders	Slides (updated on 3/16/04) Download: Ptolemy II 3.0.2 Release Window Installer (Recommended)
February 26	Tool: Ptolemy II - Multi-Modal Systems Guest: Eric Manders	Slides (updated on 3/16/04) Download: Ptolemy II 3.0.2 Release Window Installer (Recommended)
March 2	Presentation: Paper
March 4	Presentation: Paper
March 9	No Class	Spring Break
March 11	No Class	Spring Break
March 16	Computation: Hybrid Automata Tool: d/dt	Slides (updated on 3/17/04)
March 18	Discussion: Projects
March 23	Verification: Temporal Logic Guest: Sherif Abdelwahed	Slides (updated on 4/1/04)
March 25	Verification: Model Checking Guest: Sherif Abdelwahed	Same as above
March 30	Discussion: Projects
April 1	Verification: Time Automaton Application: Sensor Network	Slides (updated on 4/1/04)
April 6	Verification: Time Automaton	Slides (updated on 4/19/04)
April 8	Verification: Time Automaton	Same as above
April 13	Verification: Time Automaton	Same as above
April 15	Verification: Time Automaton	Same as above
April 20	Summary: Hybrid Automaa	Slides (updated on 4/20/04)
April 22	Computation: Linear Systems Tool: Requiem,d/dt ,Checkmate
April 27	Computation: HSIF
May 11	Presentation: Project

Presentation Schedule:

• Tuesday: Mei, Qiaozhu; Campbell, Christina Louise; Nordstorm, Steve
• Thursday: Amundson, Isaac Edward; Dubey, Abhishek; Rochelle, Stephen David

Projects

Please visit this link to download related files.

Project titles will be posted soon. Details of the projects will be discussed on March 18, 2004. 

Links:

• Hybrid Systems Course offered at 
  • University of California at Berkeley
    • Spring 2003
    • Spring 2002
    • Spring 2001
    • Spring 2000
    • Spring 1999
  • Stanford University by Claire J. Tomin
  • University of Pennsylvania by Rajeev Alur and George Pappas

• Online Communities (these sites have lots of further links to Hybrid Systems topics)
  • Virtual Action Group on Hybrid Dynamic Systems for the IEEE's Control Systems Society technical committee on Computer Aided Control System Design.
  • IEEE CSS Technical Committee on Hybrid Systems
• Research Groups
  • Center for Hybrid and Embedded Systems at Berkeley
  • Hybrid Systems Group at the University of Pennsylvania
  • Control and Optimization of Hybrid and Embedded Systems Group at the University of Siena
  • Hybrid Systems Laboratory at Stanford
• Tools
  • CheckMate for verifying hybrid systems.
  • Requiem for verifying hybrid systems.
  • d/dt for verifying and synthesis hybrid systems.
  • HyTech for verifying linear hybrid systems.
  • Ptolemy II for simulating concurrent, embedded and hybrid systems.
  • What else?
• Conferences and Workshops
  • Hybrid Systems: Computation and Control 2004 in Philadelphia.
  • Hybrid Systems: Computation and Control 2003 in Prague.
  • IFAC Conference on Analysis and Design of Hybrid Systems in France.
  • IEEE Conference on Decision and Control in Maui.