Lecture: Modeling and Analysis of Hybrid Systems

News

The lecture will start as planned on Tuesday April 07, 2020, but it will be kept (at least for the beginning) fully online. All information and learning materials will be provided in Moodle.

Prequisites:Basic knowledge in automata theory
SWS:3+1
Lecture times:Monday 12:30 – 13:15 (online)
Tuesday 16:30 – 18:00 (online)
Exercise:Monday 13:15 – 14:00 (online)
Language:English or German (depending on the students’ preferences)
Start:07.04.2020
Exam:1st exam: TBA
2nd exam: TBA
Contact:Prof. Dr. Erika Abraham
Dr. Stefan Schupp

To deepen the lecture contents, weekly exercise sheets will be distributed and can be handed in before the exercises for correction. We provide sample solutions for the exercises, video recordings, the slides of the lecture, and a lecture script in Moodle (registration to the lecture required).

What are hybrid systems?

Hybrid systems are systems with mixed discrete and continuous behavior. 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 modelling and analysis?

The behavior 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 synthesis and analysis is of high importance.

Lecture content

In this lecture, we learn how to model hybrid systems and how to analyze the behavior of the models using formal methods. More precisely, we will learn methods to solve the reachability problem, i.e. the problem to decide whether any state from a given target set is reachable in a model.

We start with introducing hybrid automata as a modeling language for hybrid systems, define several sub-classes of hybrid automata with increasing expressive power, and for each sub-class we discuss whether the reachability problem is decidable, and develop algorithms for their analysis. Besides exact methods, we consider also over-appoximative computations. Finally, we discuss extensions of hybrid automata models and their analysis methods to cover also random (probabilistic) aspects of hybrid systems.

Exams

Here we will make past exams available.

Evaluation

SS 10: lecturer and lecture (ss10)
SS 11: lecturer (ss11)lecture (ss11)
SS 12: lecturer (ss12)lecture (ss12)
SS 13: lecturer (ss13)lecture (ss13)
SS 14: no lecture (sabbatical)
SS 15: lecturer+lecture (ss15)
SS 16: lecturer+lecture (ss16)
SS 17: lecturer+lecture (ss17)
SS 18: lecturer+lecture (ss18)
SS 19: lecturer+lecture (ss19)
SS 20: lecturer+lecture+exercise (ss20)