News

  • (New) There is a discussion hour starting from 14:00 on Feb.15 in Room 4207. You are welcome to ask questions.
  • (New) The corrected exercise sheets are available at the secretary now.
  • The lecture on January 24 hat to be canceled. Due to the cancellation,  only Question 1 of Exercise 11 is required to finish before Jan. 25.
  • The slides for Lecture 16 have been updated. The definition for a periodic state has been modified. Besides, Ps(n) on slide 19 should be Ps,s(n).
  • The evaluation form is online.
  • The lecture on January 15 has been cancelled.
  • Exercise 4 of the 5th sheet is postponed until November 30th
  • The exercise class on November 16 has to be cancelled. Solutions to Series 4 of the exercises should be submitted to the secretary of Info 2 by the end of Friday, Nov. 16.
  • Exercises 3 and 4 on the 2nd sheet are postponed until November 9.
  • The lectures on October 18 and 25 have been cancelled. Thus the first Thursday lecture will be on November 8.
  • The first exercise class will take place on October 26.


Schedule

Type

Day

Time

Place

Start

Lecturer

V4

Tue

14:00-15:30

AH 2

October 16

Katoen, Noll

Thu

13:30-15:00

AH 1

November 8

Katoen, Noll

Ü2

Fri

10:00-11:30

AH 2

October 26

Neuhäußer, Han


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 of reactive 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

  1. Introduction
  2. Milner's Calculus of Communicating Systems (CCS)
  3. Equivalence of CCS Processes
  4. Case Study: the Alternating-Bit Protocol
  5. Stochastic Processes
  6. Probabilistic Process Algebra
  7. Equivalence of Probabilistic Processes
  8. Probabilities and Nondeterminism
  9. Markovian Process Algebra


Prerequisites

Basic knowledge of the relevant undergraduate courses of the first two years (Vordiplom/Bachelor) is required:

  • Automata Theory
  • Mathematical Logic
  • Discrete Mathematics
  • Probability Theory


Slides and exercise sheets (first part)

Date

Lecture

Subject

Slides

Handout

Exercise Sheet

Solution

October 16

1

Introduction

here

here

here

here

October 23

2

Semantics of CCS

here

here

October 30

3

Equivalence of CCS Processes

here

here

here

here

November 6

4

Definition of Strong Bisimulation

here

here

here

here

November 8

5

Properties of Strong Bisimulation

here

here

here

here

November 13

6

Decidability of Strong Bisimulation

here

here

-

-

November 15

7

Strong Simulation and Weak Bisimulation

here

here

here

here

November 20

8

Observation Congruence

here

here

November 22

9

Decidability of Observation Congruence

here

here

here

here

November 27

10

The Alternating Bit Protocol

here

here

November 29

11

Extensions of the Alternating Bit Protocol

here

here

here

here

(slides)

December 4

12

The Monadic π-Calculus

here

here

December 6

13

The Polyadic π-Calculus with Process Calls

here

here

here

here

December 11

14

Bisimulation in the π-Calculus

here

here


Further information

  • The course will be entirely given in English. The slides and other course material will also be in English. There are no lecture notes (yet); the course material will consist of slides.

  • The oral examination for both the Diplomstudiengang Informatik (Leistungsnachweis) and the Master program Software Systems Engineering (Theoretical CS or Specialization Subject) will take place at two alternative dates at the candidates' choice:

    • Thursday, February 21st or
    • Wednesday, March 26th.

    Please register via an e-mail to Thomas Noll. Master students additionally have to register at ZPA beforehand. The exam will be awarded with 8 ECTS credits.

  • The evaluation form is online.


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