Cyber-Physical Systems - Hybrid Models (Lecture)

News

Description

The course provides an introduction to hybrid systems, i.e., systems with discrete-continuous behavior, their mathematical semantics in terms of transition systems and traces, and the formal, logic-based verification of their temporal-logic properties.  The course generalizes, and assumes, the material of the course "Cyber-Physical Systems - Discrete Models".  In addition to the concepts and techniques of model checking of temporal-logic properties for discrete systems, the course assumes the concepts and techniques from the mathematical areas of linear arithmetic and differential equations. Most importantly, the course assumes the ability of handling the formal concepts needed to reason about programs, logical formulas and their semantics.  To take the lecture will not make sense if the student has not yet taken the lecture "Formal Methods for Java" or "Program Verification".

• 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

Here you find the list of exercise sheets.

Literature

We will use the lecture script by Erika Ábrahám and the book "Principles of Model Checking" by Christel Baier and Joost-Pieter Katoen (MIT Press, 2008); we assume the chapters in the book that have been covered in the course "Cyber-Physical Systems - Discrete Models".

Additionally we will use the following research articles:

Predicate abstraction for program verification

What's decidable about hybrid automata?

The admission criterion for the final exam is the successful participation in the exercises. The formal criterion for evaluating the successful participation in the exercises is that you present a solution for every exercise sheet (individually, no group solution).

We follow the concept of a "flipped classroom" where the student reads the relevant part of the lecture script and solves each exercise sheet in the week before the corresponding material is discussed in class.  This entails that the student reads the part of the script that introduces the corresponding material.  In the class, we will discuss the issues that have appeared while working on the exercise/the corresponding material.  For this purpose, each student will prepare a set of questions for each upcoming class.  Thus, to start the process, in the first week of the semester each student will solve the exercises on Sheet 1.  This entails that the student will read Chapter 2 of the lecture script.  Each student will send the solution (as a PDF file) to Christian Schilling until Friday, April 28, 23h59.  We will discuss the corresponding material (and the solutions) in the classes (and the exercise lesson) of the second week of the semester.  Thus, the classes/exercise lessons in this way will start on Thursday, May 4th.  In the class on the Thursday of the first week, i.e., on April 27, we will explain the topic and the organization of the lecture.