You are here: Home Teaching Summer Term 2016 Cyber-Physical Systems - Hybrid …

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.
Course type Lecture
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
Credits 6
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)

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

Exercise sheets

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.

Exercise sheet
due
 discussed
Sheet 1
 Tue, April 26
 Fri, April 29
Sheet 2
 Tue, May 3
 Fri, May 6
Sheet 3
Tue, May 10
 Fri, May 13
Sheet 4
Tue, May 24
Fri, May 27
Sheet 5
Tue, May 31
Fri, June 3
Sheet 6
Tue, June 7
Fri, June, 10
Sheet 7
Tue, June 14
Fri, June 17
Sheet 8
Tue, June 21
Fri, June 24
Sheet 9
Tue, June 28
Fri, July 1
Sheet 10
Tue, July 12
Fri, July 15
Sheet 11
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
Introduction
Fri, April 22
Supervised session (work on exercise sheet 1)
Tue, April 26
Hybrid systems
Fri, April 29
Tutorial (exercise sheet 1)
Tue, May 3
Temporal logics
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
Whitsun break
Fri, May 20
Whitsun break
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
Recapitulation
Tue, July 19
Abstraction refinement
Fri, July 22
Abstraction refinement (part 2), Tutorial (exercise sheet 11)

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

Students may discuss questions in the private Google group. To gain access, please send us your email address. Note that the email address must be associated with a Google account.

Formalia

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.