Theoretische Informatik

Communication and Parallel Processes


Next edition: Summer 2014.

The theory of communicating and concurrent agents belongs to the core of theoretical computer science. The goal of the course is to provide formalised foundations for the concept of a process lurking behind any modern software or hardware system, from an operating cycle of a vending machine to the core processes behind the UNIX command line.

In this course we provide the basics of this theory, taking as the starting point Milner's calculus of Concurrent Communicating Systems (CCS). In contrast to its close counterpart, automata theory, the theory of communicating processes is focused on behaviours of systems rather than on formal languages corresponding to them. This leads to a presentation of agents as branching structures generated by recursive definitions in a somewhat similar way as regular languages are generated by regular expressions. The resulting framework that we consider combines the following features:

  • A pseudo-programming language focusing on the most crucial concurrent primitives;
  • Isolation of basic principles and techniques for reasoning about processes;
  • Focusing on a very simple paradigm of synchronous handshakes by reading/writing messages through a channel.

Based on the elementary case of CCS we discuss formalisations of real-world examples, equivalence of formalized multi-agent systems by using the fundamental notion of bisimulation and formal verification of properties of processes.

Further on, we move to a more advanced successor of CCS, the pi-calculus, extending CCS by allowing for dynamic name creation and process replication.

Finally, we consider various systems of Modal logic associated to the process calculi such as Linear temporal logic, Computational tree logic and the Modal mu-calculus. We study by numerous examples of how process calculi can be used in conjunction with process logics for verification, i.e. for specifying and proving properties of processes.