Cyber-Physical Systems - Hybrid Models (Lecture)
In this lecture, we investigate different methods and algorithms used to model and analyze cyber-physical systems. We use the formalism of hybrid automata to account for the discrete and the continuous aspects of the system behavior.
|Instructors||Prof. Dr. Andreas Podelski, Christian Schilling
|Lecture||Tuesday, 16:00–18:00, building 101, SR 01-016
Friday, 14:00–15:00, building 101, SR 01-016
|Exercise||Friday, 15:00–16:00, building 101, SR 01-016
|First session||Tuesday, April 19, 2016, 16:00|
|Language of instruction||English
|Exam||Oral exam, September 20, 2016, building 052, room 00-017|
| Course catalog
|| Cyber-Physical Systems – Hybrid Models (Lecture)
Cyber-Physical Systems – Hybrid Models (Exercise)
- 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
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).
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.
|| Tue, April 26
|| Fri, April 29
|| Tue, May 3
|| Fri, May 6
||Tue, May 10
|| Fri, May 13
||Tue, May 24
||Fri, May 27
||Tue, May 31
||Fri, June 3
||Tue, June 7
||Fri, June, 10
||Tue, June 14
||Fri, June 17
||Tue, June 21
||Fri, June 24
||Tue, June 28
||Fri, July 1
||Tue, July 12
||Fri, July 15
||Tue, July 19
||Fri, July 22
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).
|Tue, April 19
|Fri, April 22
||Supervised session (work on exercise sheet 1)
|Tue, April 26
|Fri, April 29
||Tutorial (exercise sheet 1)|
|Tue, May 3
|Fri, May 6||Temporal logics (part 2), Tutorial (exercise sheet 2)
|Tue, May 10||Timed automata|
|Fri, May 13
||Tool demo "UPPAAL", Tutorial (exercise sheet 3)|
|Tue, May 17
|Fri, May 20
|Tue, May 24
||TCTL model checking
|Fri, May 27
||TCTL model checking (part 2), Tutorial (exercise sheet 4)
|Tue, May 31||Reachability analysis
|Fri, June 3
||Reachability analysis (part 2), Tutorial (exercise sheet 5)
|Tue, June 7||Predicate abstraction
|Fri, June 10||Predicate abstraction (part 2)
|Tue, June 14||Rectangular automata, Tutorial (exercise sheet 6)
|Fri, June 17||Rectangular automata (part 2), Tutorial (exercise sheet 7)|
|Tue, June 21||Rectangular automata (part 3)
|Fri, June 24
||Rectangular automata & Predicate abstraction
|Tue, June 28
||Linear hybrid automata, Tutorial (exercise sheets 8 & 9)|
|Fri, July 1
||Linear hybrid automata (part 2)
|Tue, July 5
||Linear hybrid automata (part 3)|
|Fri, July 8||"Faculty summer party"
|Tue, July 12||Tutorial (exercise sheet 10), Tool demo "SpaceEx"|
|Fri, July 15
|Tue, July 19
|Fri, July 22
||Abstraction refinement (part 2), Tutorial (exercise sheet 11)
We use the lecture script by Erika Ábrahám.
Christel Baier, Joost-Pieter Katoen, Principles of Model Checking, MIT, 2008, ISBN 9780262026499
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.