In this lecture we address foundations of the modeling and analysis of hybrid systems. Information for the summer semester 2011:
|
Prerequisites:
|
Basic knowledge in automata theory
|
|
SWS:
|
3+1
|
|
Lecture times:
|
Tuesday 13:15 – 14:15 (room 5056)
|
|
Friday 13:15 – 14:30 (room 5056)
|
|
|
Exercise:
|
Tuesday 14:15 – 15:00 (room 5056)
|
|
Start:
|
April 05, 2011
|
|
Language:
|
English or German (depending on the students’ preferences)
|
|
Exam:
|
Oral
|
|
ECTS credits:
|
6
|
To deepen the lecture contents, weekly exercise sheets should be solved in two-men-groups. We provide sample solutions for the exercises, the slides of the lecture, and a lecture script in L2P. Registration in the campus system is required.
What are hybrid systems?
Hybrid systems are systems with mixed discrete and continuous behaviour. Typical examples are physical systems which continuously evolve over time and are controlled by some discrete controller, e.g., a chip or a computer.
 |
Why modeling and analysis?
The behaviour of hybrid systems is often safety-critical. For example, in case of an accident an airbag can save the life of the car driver, but only if the airbag reacts in time. To assure the correct functioning of such safety-critical hybrid systems, their automatic analysis is of high importance.
Lecture content
In the lecture we first introduce hybrid automata to model hybrid systems. Then we define certain classes of hybrid automata with increasing expressive power. For each class we discuss whether the reachability problem is decidable and develop algorithms for their analysis. Finally we discuss methods for the over-appoximative representation of state sets and show how they can be used for reachability analysis.
The slides of the last lecture (SS 2010):
|
Nr.
|
Theme
|
Slides
|
||||||
|
1.
|
|
|
Introduction
|
 |
||||
|
2.
|
|
|
The modeling of hybrid systems
|
 |
||||
|
3.
|
|
|
Classes of hybrid automata and algorithms for their analysis
|
|||||
|
3.1
|
Discrete systems
|
 |
||||||
|
3.2
|
Timed automata
|
 |
 |
|||||
|
3.3
|
Rectangular automata
|
 |
||||||
|
3.4
|
Linear hybrid automata
|
 |
||||||
|
4.
|
|
|
Over-approximative state set representation and reachability analysis
|
 |
||||
|
||||||||
|
4.1
|
Convex polyhedra
|
 |
||||||
|
4.2
|
Orthogonal polyhedra
|
 |
||||||
|
4.3
|
Oriented rectangular hulls
|
 |
||||||
|
4.4
|
Using those approximations in the reachability analysis
|
 |