Modelling and Analysing Concurrent Systems

Course at XXVIII Rio Summer School of Informatics

Rio Cuarto, Argentina; February 13-17, 2023


The aim of this course is to provide a basic understanding of modelling formalisms for concurrent systems. It will follow the so-called interleaving approach, which reduces the phenomenon of concurrency to a non-deterministic merging of sequential executions of sub-processes. This method is represented by Milner’s Calculus of Communicating Systems, a process algebra which provides a mathematical basis for describing both the structure and the behaviour of systems in a compositional way. To support formal reasoning about their correctness properties, we will introduce behavioural equivalences and logic-based techniques, and will demonstrate their tool-based application on mutual-exclusion algorithms.


    1. Milner’s Calculus of Communicating Systems
    2. Behavioural Equivalences
    3. Logical Specifications
    4. Application: Mutual-Exclusion Protocols


    Thomas Noll