News
- (new) 23.07.2009: The solutions of ex9 and ex10 are available.
- 19.07.2009: The lecture and exercise class on July 22-23 are switched.
- 13.07.2009: There are no exercise class on 15.07, the next (and the last) one will be on 23.07, 15:00.
- 13.07.2009: The solution of ex8 can be found here.
- 10.07.2009: The evaluation results are online.
- 09.07.2009: The 4th question in ex8 has been updated.
- 02.07.2009: The next exercise class will take place at 13:00 on July 13 instead of July 8.
- 02.07.2009: The solution of ex7 can be found here.
- 02.07.2009: The algorithms for deciding strong simulation in DTMCs can be found in Section 4 in this paper.
- 19.06.2009: From next week on, both the lecture and the exercise class will take place in the seminar room of i2, i.e., Room 4201b.
- 14.05.2009: Solution for exercise 2.1b
- 06.05.2009: Lecture and exercise class on May 13-14 are switched
- 30.04.2009: Friday lecture moved ahead by 30 mins (starting May 8)
- 13.02.2009: web page is launched
Schedule
Type
Day
Time
Place
Start
Lecturer
Overview
The aim of this course is to provide a basic understanding of modeling formalisms for reactive systems. In contrast to sequential systems whose meaning is defined by the results of finite computations, the behaviour of reactive systems is mainly determined by communication, interaction, and mobility of non-terminating processes.
Traditionally, models and methods for the analysis of the functional correctness ofreactive systems and those for the analysis of their performance and dependability aspects, have been studied by different research communities. This has resulted in the development of successful, but distinct and largely unrelated modeling and analysis techniques for both domains. In many modern systems, however, the difference between their functional features and their performance properties has become blurred, as relevant functionalities become inextricably linked to performance aspects. The strong relationship between functionality and performance aspects calls for a modeling and analysis approach in which qualitative and quantitative aspects are studied from an integrated perspective.
This need has resulted in combining insights and results from process algebra with techniques for performance modeling and analysis such as Markov chains. Process algebra provides a formal apparatus for reasoning about structure and behavior of systems in a compositional way. Process algebras and their probabilistic extensions are aimed to overcome the lack of hierarchical, compositional facilities in performance modeling and form the central theme of this course.
Contents
No. | Date | Topic | Slides | Handout | Exercises |
|---|---|---|---|---|---|
1 | April 23 | Introduction | |||
2 | April 24 | Semantics of CCS | |||
3 | April 30 | Equivalence of CCS Processes | |||
4 | May 7 | Trace Equivalence | |||
5 | May 8 | Strong Bisimulation | |||
6 | May 13! | Properties of Strong Bisimulation | |||
7 | May 15 | Decidability of Strong Bisimulation
& Definition of Strong Simulation | |||
8 | May 22 | Weak Bisimulation | |||
9 | May 28 | Observation Congruence | |||
10 | May 29 | The Alternating-Bit Protocol | |||
11 | June 12 | Extensions of the Alternating-Bit Protocol | |||
12 | June 18 | Stochastic Processes | |||
13 | June 19 | Discrete-time Markov Chains | |||
14 | June 25 | Probabilistic Bisimulation | |||
15 | June 26 | Probabilistic Simulation 1 | Here(updated) | ||
16 | July 2 | Probabilistic Simulation 2 | |||
17 | July 3 | Probabilistic Process Algebra | until July 13 (updated) | ||
18 | July 9 | Bisimulation and Parallel Composition | |||
19 | July 10 | Probabilistic Automata | |||
20 | July 16 | Continuous-Time Markov Chains | |||
21 | July 17 | (Bi)simultion on CTMCs | |||
22 | July 22 | Markovian Process Algebra |
Prerequisites
Basic knowledge of the relevant undergraduate courses of the first two years (Vordiplom/Bachelor) is required:
- Automata Theory (in particular, finite and pushdown automata)
- Discrete Mathematics
- Probability Theory
Further information
- The course will be entirely given in English.
- There are no lecture notes (yet); the course material will consist of slides.
- The exam will be awarded with 8 ECTS credits. Details will follow later.
Additional background literature
- R. Milner: Communicating and Mobile Systems: the pi-Calculus. Cambridge University Press, 1999
- R. Milner: Communication and Concurrency. Prentice Hall, 1989
- H.C. Tijms: A first course in stochastic models. Wiley, 2003
- J. Bergstra, A. Ponse, S.A. Smolka: Handbook of Process Algebra. Elsevier, 2001 (Chapters 6 and 11)
- J. Hillston: A Compositional Approach to Performance Modelling. Cambridge University Press, 1996
- H. Hermanns: Interactive Markov Chains: The Quest for Quantified Quality. LNCS 2428, Springer 2002
- E. Brinksma, H. Hermanns, J.-P. Katoen: Lectures on Formal Methods and Performance Analysis. LNCS 2090, Springer 2001