Modelling and analysis of hybrid systems

In this lecture we address foundations of the modeling and analysis of hybrid systems. Information for the summer semester 2013:

Prequisites:

Basic knowledge in automata theory

SWS:

3+1

Lecture times:

Tuesday 13:15 – 14:15 (room 5056)

Friday 13:30 – 14:45 (room 5056)

Exercise:

We offer two exercise dates, between which you may choose:

Tuesday 14:15 – 15:00 (room 5056)

Friday 15:00 – 15:45 (room 5056)

Start:

April 09, 2013

Language:

English or German (depending on the students’ preferences)

Exam:

Written

ECTS credits:

6

To deepen the lecture contents, weekly exercise sheets should be solved in two-men-groups and handed in before the exercises. We provide sample solutions for the exercises, video recordings, the slides of the lecture, and a lecture script in L2P. Registration in the campus system and in L2P 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 synthesis and analysis is of high importance.

Lecture content:

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

Current lecture slides (might be modified during the semester):

Nr. 

Theme

 Slides

1.

Introduction 

00_intro_annotated

2.

The modeling of hybrid systems

01_hybrid_annotated

3. 

Propositional and temporal logics 

02_discrete_annotated

4. 

Timed automata 

03_timed_annotated

5.

Model checking on timed automata 

04_mc_timed_annotated 04_mc_timed_annotated_18.05

6. 

Rectangular automata

05_rectangular_annotated 05_rectangular_annotated_18.05

7. 

Linear hybrid automata 

06_linear_annotated 08_approximation_annotated

8. 

Reachability analysis of hybrid automata 

07_analysis_annotated

9. 

 Representations of the reachable sets

 09_reachability_analysis_annotated

9.1. 

Convex polyhedra 

10_polyhedra_annotated

9.2. 

Orthogonal polyhedra

11_orthogonal_polyhedra_annotated

Evaluations