Cyber-Physical Systems - Hybrid Models
We will investigate different methods and algorithms used to model and analyze cyber-physical systems. We will use the formalism of hybrid automata in order to account for the discrete and the continuous aspects of the behavior of cyber-physical systems.
Description
The lecture will cover the following topics:
- Modelling of cyber-physical systems by hybrid automata
- Specification of properties of cyber-physical systems in temporal logics
- Analysis and verification algorithms
News
- Due to a holiday on Thursday, the 7th of June, next week on Tuesday, the 12th of June, there will a lecture session instead of an exercise group. Thus you will have one more week to prepare your exercise sheet.
- There will be no lecture (and no exercise group) on Tuesday, 1.5.2012 which is a holiday in Germany.
- The first lecture will be held on Tuesday, 24.4.2012, at 16h. This will be an introductory lecture; exceptionally there will be no exercise group.
- In the first week, we will hand out an exercise sheet with exercises on material that you will acquire in the three lectures of the first two weeks. I.e., the lectures of the three lectures in the first two weeks will cover the material that you need in order to be able to solve the exercises that you received at the beginning of the first week. You will hand in the solutions until the lecture on on Tuesday, 8.5.2012. The first half of the lecture on Tuesday, 8.5.2012, is the (first) exercise group. In this exercise group, we will discuss the exercises of the first exercise sheet.
Exercises
At the beginning of each week, we will hand out an exercise sheet with exercises on material that you will acquire in that week. I.e., the lectures of each week will cover the material that you need in order to be able to solve the exercise sheet that you received at the beginning of the week. In each new week, we start with the exercise group to discuss the exercises which you have worked on during the preceding week.
Exercise Submission Scheme
- You will have one week to hand in the solutions of the exercises, i.e., the time from the beginning of the week until the tuesday of the following week. There will be a designated lockbox in building 051 floor 00 which we will empty it at 16h10 sharp. You can also hand in the solutions at the beginning of the exercise group at 16h15.
- You will hand in a signed sheet with the solutions of every exercise sheet. You will hand in whatever you have been able to do, possibly nothing if you were sick. In case you have been sick, you just mark this on your signed solution sheet.
- The first half of the tuesday lecture is the exercise group. In this exercise group, we will discuss the exercises which you have worked on during the preceding week and for which you have just handed in the solutions.
- We will adapt the above scheme where needed (initialization, holidays, ...).
Admission to final exam
Admission criteria for the final exam are 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 handed in a signed sheet with the solutions of every exercise sheet. As said above, you will hand in whatever you have been able to do, possibly nothing if you were sick. In case you have been sick, you just mark this on your signed solution sheet.Resources
Slides
Lecture 1.Lecture 3.
Lecture 4.
Lecture 5.
Lecture 6.
Lecture 7.
Lecture 8.
Lecture 9.
Lecture 10.
Lecture 11.
Exercise sheets
You can find slides used to revise LTL and CTL in scope of exercise group here.