CyberPhysical Systems I  Discrete Models
In this course we demonstrate how cyberphysical systems, in the wide range of their heterogeneous aspects (largescale systems, system of systems, embedded systems, concurrent systems, hardware systems, software systems) can be modeled using the basic notion of transition systems. We consider relevant formalisms for modeling correctness properties of cyberphysical systems, and show how the models can be analyzed using algorithmic methods in order to prove correctness or find errors.
Course type  Lecture 

Instructors  Prof. Dr. Andreas Podelski, Tanja Schindler 
Lecture  Wednesday, 16:00  18:00, building 101 HS 00036 
Exercise  Monday, 12:00  14:00

Language of instruction  English 
Credits  6 
Exams  Written exam 
Course catalog  CyberPhysical Systems – Discrete Models  Lecture CyberPhysical Systems – Discrete Models  Exercises 
News
 Nov. 29: Sheet 6 was updated, there was a mistake in Ex.1 (g) (wrong alphabet).
 Nov. 18: Small change in Sheet 5: Exercise 2 (c) has been replaced by a slightly different task.
 Oct. 27: Sheet 3 is online. You will have time until Nov. 10 as there will be no CPS I sessions (lecture and exercises) next week. However, we recommend to start working on the material and the exercises early as it takes a lot of time.
 Oct. 27: The new sheet will be published by 7 pm today.
 Oct. 26: There will not be exercise groups on Monday, Oct. 30. You still have to submit your solutions to sheet 2 until Friday, Oct. 27, and will get a new sheet then.
 Oct. 24: Updated sheet 2. The tasks remain the same, but it should be clearer now what we expect in Ex. 2.
 Oct. 17: You can join the Ilias course via this link.
 Oct. 12: We start with a lecture on Monday, Oct. 16, 16:00  18:00, in building 101, room 00026. There are no tutorials in the first week.
From the second week on, the lecture will take place on Wednesday and the tutorials on Monday, as stated above.
Description
The course provides an introduction to discrete models of cyberphysical systems, their analysis and verification: The students learn how to model cyberphysical systems as transition systems. Here, the main focus lies on software and hardware aspects of cyberphysical systems and on methods for modeling parallelism and communication.
 Moreover, the students learn how to express properties about such systems. The course covers different mechanisms to specify temporal properties including linear time properties and branching time properties such as LTL, CTL, and CTL* properties.
 Finally, the course demonstrates how to develop algorithms for checking whether these properties hold. After presenting algorithms for explicit state systems we introduce symbolic BDDbased algorithms which are able to tackle the wellknown "state explosion problem". In addition, the course covers basic "Bounded Model Checking" (BMC) techniques which restrict the analysis to computation paths up to a certain length and reduce the verification problem to a Boolean satisfiability problem.
Course
We follow the concept of a "flipped classroom" where the student
reads
the relevant part of the course material before it is discussed in
class. The exercises should give an orientiation on what to focus while
working through the material. Each student will prepare a
set of questions for each upcoming class.
Exercises
The lecture is accompanied by exercises. Each Friday we will publish an exercise sheet. Students will have time until the next Friday to prepare solutions for the problems stated on the exercise sheet. Submissions in groups of two are strongly encouraged. The solutions have to be submitted by 11:59 am via the post boxes that are located in the ground floor of building 051. The solutions will be corrected by the tutors and discussed in the exercise groups on Monday.
Exam
There will be a written exam at the end of the semester. Prerequisite for admission to the final exam is an active participation in the exercises. You have to submit solutions to every exercise sheet and present at least one exercise in the discussions at the exercise group.
You may bring to the exam one DIN A4 sheet. Both sides of this sheet may be filled with any notes (e.g., definitions, theorems, examples) but the notes have to be handwritten. You must not use any other material in the exam (except for writing utensils).
The duration of the exam will be 90 minutes.
You may bring to the exam one DIN A4 sheet. Both sides of this sheet may be filled with any notes (e.g., definitions, theorems, examples) but the notes have to be handwritten. You must not use any other material in the exam (except for writing utensils).
The duration of the exam will be 90 minutes.
Resources
Exercise sheets
Here you find the list of exercise sheets.
Exercise sheet 
Literature 

Sheet 1 
pp. 19  29 
Sheet 2  pp. 29  35 pp. 915  920 (A.3) 
Sheet 3  Sects. 2.2.1 and 2.2.2 A.1 and A.2 
Sheet 4 
Sect. 2.2.3 and A.2 
Sheet 5 
Sect. 2.2.4 
Sheet 6  Sect. 3.2 to (incl.) 3.2.3 
Sheet 7  Sects. 3.3.1 and 3.3.2 
Sheet 8  Sect. 3.4 Sects. 3.2.4 and 3.3.3 
Sheet 9  Sect. 3.5 
Old slides
You can find slides from last year's lecture on the corresponding webpage. (You need a login.)
Literature
The lecture will follow very closely the famous textbook "Principles of Model Checking" by Christel Baier and JoostPieter Katoen (MIT Press). A copy is available in the library.