Uni-Logo

Cyber Physical Systems - Discrete Models

Due to a scheduling conflict, the time slot for the exercise is moved to Monday and the lecture time on Thurday needs to be adjusted slightly. See the new dates/times below. The new lecturing schedule is effective from 9 January.

The course provides an introduction to discrete models of cyber-physical systems, their analysis and verification.

The students learn how to model cyber-physical systems as transition systems. Here, the main focus lies on software and hardware aspects of cyber-physical systems and on methods for modeling parallelism and communication.

Moreover, the students learn how to express properties of such systems. The course covers different mechanisms to specify temporal properties including linear time properties and branching time properties using logical formalisms such as LTL, CTL, and CTL*.

Finally, the course demonstrates how to develop algorithms for checking whether these properties hold.

LecturerProf. Dr. Peter Thiemann
Time and PlaceMo 16-16:45 (s.t.!),SR 01-009/13, Geb. 101
Do 12-13:45 (s.t.!), SR 01-009/13, Geb. 101
Assistants Manuel Geffken

Robert Jakob

Exercise

Time and PlaceMo 17-17:45 (s.t.!) SR 01-009/13, Geb. 101

In addition to the lecture, we will publish exercise sheets. These exercise sheets are mandatory and ensure that you work on and understand the topics presented in the lecture. If you were not able to do the exercise, please hand in your partial results with a statement why you couldn't do it.

Exercise sheets are published on the Piazza course homepage.

Exam

Details about the exam (either oral or written) are yet to be announced.

Form and Questions

This course uses the learning and teaching platform Piazza (similar to a forum).

Please enroll there using the following link https://piazza.com/uni-freiburg.de/winter2014/11le13vid120948.

The course homepage of Piazza can be seen here: https://piazza.com/uni-freiburg.de/winter2014/11le13vid120948/home.

Literature

The lecture's main source is the well-known model checking book (there are 10 copies in the library) of Baier and Katoen.