Modelling Concurrent Systems WS 05/06

Graduate Course - Winter Term 2005/06
Lehrstuhl für Informatik 2

News

07.02.2006: The results of the evaluation of the lecture and of the exercise course are available.
31.01.2006: The exercise course on February 6th is cancelled.
20.12.2005: The written exam is scheduled for January 31st, 2006, at the usual time and place (Tue 11:40-13:00, AH I) of the lecture.
01.11.2005: Because of the "Fachschaftsvollversammlung", the lecture on November 8th has to be cancelled.

Exam

Schedule

Type	Time	Place	Start	Lecturer
V2	Tue 11:40-13:00	AH I	18.10.	Noll
Ü1	Mon 13:45-15:15	AH II	31.10. (biweekly)	Noll

The aim of this course is to provide a basic understanding of communicating and mobile systems. In contrast to sequential systems whose meaning is defind by the results of finite computations, the behaviour of concurrent systems is mainly determined by communication, interaction, and mobility of infinite processes. We analyze these notions using Milner's Calculus of Communicating Systems (CCS).

In particular, we study the equivalence of processes by means of labelled transition systems and bisimulations. Examples will illustrate the practical relevance of this approach. This course is connected to the course Model Checking in which methods for the verification of concurrent systems are studied.

Transparencies

No.	Date	Contents
1	18.10.2005	Introduction
2	25.10.2005	Calculus of Communicating Systems (CCS)
3	01.11.2005	Structural Congruence
4	14.11.2005	Semantics of CCS
5	22.11.2005	Equivalence of CCS Processes
6	29.11.2005	Definition of Strong Bisimulation
7	06.12.2005	Properties of Strong Bisimulation
8	13.12.2005	Decidability of Strong Bisimulation
9	20.12.2005	Weak Bisimulation
10	10.01.2006	Observation Congruence
11	17.01.2006	Decidability of Observation Congruence
12	24.01.2006	The Alternating Bit Protocol
13	07.02.2006	Extensions of the ABP

Exercises

No.	Issued	Presentation	Sheet
1	25.10.2005	31.10.2005/15.11.2005	here (faulty car locker)
2	15.11.2005	28.11.2005	here (improved car locker, solution Ex. 8)
3	29.11.2005	12.12.2005	here
4	12.12.2005	09.01.2006	here (solution Ex. 14)
5	10.01.2006	23.01.2006	here

Literature

R. Milner: Communicating and Mobile Systems: the π-Calculus, Cambridge University Press, 1999 (Library)
R. Milner: Communication and Concurrency, Prentice Hall, 1989 (Library)

Modelling Concurrent Systems

Graduate Course - Winter Term 2005/06 Lehrstuhl für Informatik 2