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, Dr. Matthias Heizmann, Christian Schilling 
Lecture  Monday, 16:00  18:00, building 101 HS 00026 Wednesday, 16:00  17:00, building 101 SR 00010/014 
Exercise  Wednesday, 17:00  18:00

Language of instruction  English 
Credits  6 
Exams  Written exam, on 13th March at 14:00 (s.t.) in rooms 026, 036, and 010/14 in building 101 
Course catalog  CyberPhysical Systems – Discrete Models  Lecture CyberPhysical Systems – Discrete Models  Exercise 
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.
 All necessary foundations for these algorithms such as fixed point theory, data structures like binary decision diagrams (BDDs), and satisfiability (SAT) solvers are introduced in the course as well.
News
 Mar. 27: The exam review (Klausureinsicht) takes place on Wednesday, April 19, from 2 pm to 3 pm in room 00016 of building 052.
 Mar. 13: Most likely you will be able to see the exam results in the Campus Management system starting from some day between 22nd and 24th March. (However, there is some risk that we need more time for providing the results.)
 Feb. 08: Added information about the duration of the exam (90min)
 Feb. 06: Added information about material that you may bring to the exam (A4 sheet).
 Jan. 23: Exercise 2d on sheet 12 became a bonus exercise because the property which was given in natural language was not very precise.
 Dec. 04: New "WhithoutOverlay" version of slides available. This version is a compromise between the slides (which contain many overlay frames) and the handout (which is sometimes unreadable). Many thanks to Claus Schätzle for sharing his perl scripts that transform the slides.
 Nov. 30: There was a typo in Exercise 1 on sheet 7.
 Nov. 24: There was a mistake in sheet 6 (that was corrected yesterday evening): Instead of "bad prefix of minimal total length" we accidentally wrote "minimal bad prefix".
 Nov. 2: Exercise 2 on sheet 2 became a bonus exercise.
 Oct 27: The room for the group 2 tutorial was changed (see above).
 Oct, 21: Solutions for exercises have to be submitted via the post boxes that are located in the ground floor of building 051.
 Oct, 20: From now on Monday's lecture will be in room HS 00026 in building 101.
 Oct, 19: You may submit your solutions of exercise sheets alone or in a group of two.
 Oct. 19: Until this evening the exercise groups on this website were accidentally listed in the wrong order. Please recheck the room number before you visit your exercise group.

Oct. 18:
 The application limit in the course management system (HisInOne) was raised from 80 to 100.
 The groups have been assigned. To make the group size equal, we had to move some students from group 1 to group 2. If you want to change the group, please write a mail to Christian, ideally with a suitable candidate for swapping.
Exercises
The lecture is accompanied by exercises. At the beginning of each week we will publish an exercise sheet at this website. Students will have time until the next Monday to prepare solutions for the problems stated on the exercise sheet. The solutions have to be submitted before the start of the lecture 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 Wednesday.
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. A sufficient criterion for an active participation is that you received 50% of the exercise points and presented 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 may 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 may not use any other material in the exam (except for writing utensils).
The duration of the exam will be 90 minutes.
Resources
Slides
date  slides  handout  topics  

Mon, October 17 
Introduction 

Wed, October 19 
lec02slides.pdf 
lec02handout.pdf 
Formal verification, Transition systems, Transition systems for sequential circuits 

Mon, October 24 
lec03slides.pdf 
lec03WithoutOverlays.pdf  lec03handout.pdf 
Program graphs, Transition systems for program graphs, Guarded Command Language 
Wed, October 26 
lec04slides.pdf  lec04WithoutOverlays.pdf  lec04handout.pdf  Guarded Command Language, Spin 
Mon, October 31 
lec05slides.pdf  lec05WithoutOverlays.pdf  lec05handout.pdf  Parallel systems, Interleaving operator 
Wed, November 2 
lec06slides.pdf  lec06WithoutOverlays.pdf  lec06handout.pdf  Parallel systems, Synchronization operator, Nondeterminism 
Mon, November 7 
lec07slides.pdf  lec07WithoutOverlays.pdf  lec07handout.pdf  Parallel systems, Mutual exclusion, Statebased view on transition systems 
Wed, November 9 
lec08slides.pdf  lec08WithoutOverlays.pdf  lec08handout.pdf  Statebased view on transition systems, Paths, Traces 
Mon, November 14 
lec09slides.pdf  lec09WithoutOverlays.pdf  lec09handout.pdf  Traces, Regular expressions, Omegaregular expressions 
Wed, November 16 
lec10slides.pdf  lec10WithoutOverlays.pdf  lec10handout.pdf  LT properties, Trace inclusion, Trace equivalence 
Mon, November 21 
lec11slides.pdf  lec11WithoutOverlays.pdf  lec11handout.pdf  Propositional logic, Invariants, Safety properties 
Wed, November 23 
lec12slides.pdf  lec12WithoutOverlays.pdf  lec12handout.pdf  Safety properties, Prefix closure 
Mon, November 28 
lec13slides.pdf  lec13WithoutOverlays.pdf  lec13handout.pdf  Prefix closure, Finite traces and trace inclusion, Liveness properties 
Wed, November 30 
lec14slides.pdf  lec14WithoutOverlays.pdf  lec14handout.pdf  Fairness 
Mon, December 5 
lec15slides.pdf  lec15WithoutOverlays.pdf 
lec15handout.pdf  Fairness, Finite automata (NFA), Regular safety properties 
Wed, December 7 
lec16slides.pdf  lec16WithoutOverlays.pdf  lec16handout.pdf  Regular safety properties, Ultimate automata library 
Mon, December 12 
lec17slides.pdf  lec17WithoutOverlays.pdf  lec17handout.pdf  Checking regular safety properties 
Wed, December 14 
lec18slides.pdf  lec18WithoutOverlays.pdf  lec18handout.pdf  ωregular properties, Büchi automata (NBA) 
Mon, December 19 
lec19slides.pdf  lec19WithoutOverlays.pdf  lec19handout.pdf  Equivalence of Büchi automata and ωregular expressions. 
Wed, December 21 
lec20slides.pdf  lec20WithoutOverlays.pdf  lec20handout.pdf  Nonemptiness for NBA, Generalized Büchi Automata (GNBA) 
Mon, January 9 
lec21slides.pdf  lec21WithoutOverlays.pdf  lec21handout.pdf  Checking ωregular properties 
Wed, January 11 
lec22slides.pdf  lec22WithoutOverlays.pdf  lec22handout.pdf  Intersection for GNBA, Syntax of LTL 
Mon, January 16 
lec23slides.pdf  lec23WithoutOverlays.pdf  lec23handout.pdf  Semantics of LTL 
Wed, January 18 
lec24slides.pdf  lec24WithoutOverlays.pdf  lec24handout.pdf  Weak Until, LTLPNF 
Mon, January 23 
lec25slides.pdf  lec25WithoutOverlays.pdf  lec25handout.pdf  Automatabased LTL model checking 
Wed, January 25  lec26slides.pdf  lec26WithoutOverlays.pdf  lec26handout.pdf  
Mon, January 30 
lec27slides.pdf  lec27WithoutOverlays.pdf  lec27handout.pdf  Computation tree logic 
Wed, February 1 
lec28slides.pdf  lec28WithoutOverlays.pdf  lec28handout.pdf  CTL model checking 
Mon, February 6 
 
lec29WithoutOverlays.pdf 
 
Brief summary of course content up to Lecture 17 
Wed, February 8 
 
lec30WithoutOverlays.pdf   
Brief summary of course content starting with Lecture 18. Ultimate LTL Automizer 
Examples
Lecture 21: Automata Script file for trafficlight example
Lecture 22: Automata Script file for messages example
Exercise sheets
sheet  submission 

sheet 1  Mon, October 24 
sheet 2 
Mon, October 31 
sheet 3 
Mon, November 7 
sheet 4 
Mon, November 14 
sheet 5 
Mon, November 21 
sheet 6 
Mon, November 28 
sheet 7 
Mon, December 5 
sheet 8 
Mon, December 12 
sheet 9 
Mon, December 19 
sheet 10  Mon, January 9 
sheet 11  Mon, January 16 
sheet 12  Mon, January 23 
sheet 13 
Mon, January 30 
sheet 14  Mon, February 6 
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.