No participant requirements

Introduction to Milner’s Calculus of Communicating Systems (CCS) and the π-Calculus.
Professional competence
The students:

• know the theory of the operational semantics of CCS and the π-calculus - Perform equivalence proofs using simulations and bisimulations
• specify communicating and mobile systems with CCS and the π-calculus

Methodological competence
The students:

• learn about different views on mobility
• recognize equivalences as formal means for system correctness

Social competence
The students:

• work together in small groups to solve problems
• present their solutions to groups of other students

Self-competence

• The students:
• learn persistence in pursuing difficult tasks
• learn precision in specifying problems

Communication is one of the basic concepts of computer science. It occurs between computers in a network as well as between components of a computer. The focus of the course is on Robin Milner's π-calculus. It enables a new modelling of communication, taking the location of the communication into account. The π-calculus can describe the change of data in a computer as well as the sending of messages or even programs along networks like the internet. It is also possible to describe reconfigurable networks. This will be shown using the examples of mobile phones, schedulers, automatic vending machines, data structures, communication protocols, and objects in object-oriented programming. All these applications are backed by the theory of the π-calculus, which is based on operational semantics and a concept of behavioural equivalence. The theory will be explained in a step-by-step manner.
Topics:

• different views on mobility
• transition systems with simulations and bisimulations
• Milner's Calculus of Communicating Systems (CCS) and Milner's π-calculus for mobile systems, both with operational semantics, structural congruence, strong equivalence and observational equivalence, relationship between reactions and transitions, solvability of recursive equations
• formal specification of examples of communicating and mobile systems using CCS and the π-calculus
• proof of strong equivalence and observational equivalence of given processes
• specification of dynamic data structures in the π-calculus

• Robin Milner. Communicating and Mobile Systems: The pi-calculus. Cambridge University Press, 1999.
• Robin Milner. Communication and Concurrency. Prentice Hall, 1989.
• D. Sangiorgi and D. Walker. The pi-calculus: A Theory of Mobile Systems. Cambridge University Press, 2001.

At the end of the lecture period

written exam or oral exam