Cyber-Physical Systems - Hybrid Models (Lecture)

News

• Sept 12: The oral exam takes place in Prof. Podelski's office: building 052, room 00-017.
• July 25: The date for the (oral) exam was set to September 20. Please let us know if this date does not work for you.
  
• June 13: updated slides set "Rectangular automata"
• June 10: updated exercise sheet 7
  
• June 2: added Google group for discussions
• May 24: updated slides set "TCTL model checking"
  
• May 11: updated slides set "Timed automata"
• May 4: clarified the text for exercise 3 on sheet 3 (the tasks stay the same)
  
• May 3: updated slides set "Temporal logics"
  
• Apr 26: updated slides set "Hybrid systems" and exercise sheet 2
  
• Apr 19: updated slides set "Introduction"; added a paragraph about the "flipped classroom" concept

Description

The course provides an introduction to the modeling and analysis of hybrid systems, i.e., systems with discrete-continuous behavior, from the viewpoint of computer science.

• Hybrid automata are introduced as a syntactic model for hybrid systems. Corresponding labeled transition systems are used to define their semantics.
• Timed automata, as an important subclass of hybrid automata that extend discrete systems with a notion of time are considered. The branching time temporal logic TCTL is introduced to specify properties of timed automata, and corresponding model checking algorithms are developed.
• As a further important subclass – more general than timed automata – we define linear hybrid automata. We show that the reachability problem for linear hybrid automata is in general undecidable, whereas bounded reachability, i.e., reachability within a fixed number of steps, is still decidable and can be efficiently computed. We also consider bounded reachability for general hybrid automata and discuss corresponding solution approaches.
• Finally, the course provides basic knowledge on stochastic systems and corresponding model checking algorithms. To do so, we introduce discrete-time Markov chains (DTMCs) and probabilistic computation tree logic (PCTL).

Resources

Here you find the exercise sheets including the dates of delivery and discussion. If you want to submit an electronic solution (as PDF file), please send it to Christian Schilling. Please also see the "Formalia" section below about group submissions.

Slides & Schedule

Here you find the sets of slides used in the lecture and a schedule. The schedule is provisional, so the exact contents may change dynamically. We will add more sets of slides as the course advances. The password for accessing the slides is provided in the lecture (interested students may ask us for access).

Lecture script

We use the lecture script by Erika Ábrahám.

Literature

Christel Baier, Joost-Pieter Katoen, Principles of Model Checking, MIT, 2008, ISBN 9780262026499

Predicate abstraction for program verification

What's decidable about hybrid automata?

The algorithmic analysis of hybrid systems

Discussion group

The admission criterion for the final exam is the successful participation in the exercises. We will correct your solutions but we will not grade them. There will be no 50% rule or such. The formal criterion for evaluating the successful participation in the exercises is that you have worked on every exercise sheet. You will hand in the set of solutions that you have been able to find, possibly the empty set (if you are sick, just send an email so that we know that you are still participating in the course).

We follow the concept of a "flipped classroom" where the students read the relevant part of the lecture script and work on the exercises in advance. Only after submitting the solutions will we discuss the related material in the lecture. The students are supposed to work in groups and also submit a group solution. Consequently, the lectures will be very open to questions from the audience.