Modelling and Analysing Concurrent Systems

Course at RIO 2023 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 to Mutual-Exclusion Protocols


The exam is organised in the form of a homework task, in which you have to model a simple data communication protocol. Details are given in this document. The corresponding report has to be submitted to by March 31, 2023.

Additional Material

  • Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen and Jiri Srba: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, 2007.
    • A draft version of the first part is available here.
  • Check out the CAAL Tool developed at Aalborg University, which is used in the exercises and lectures.
    • The CAAL specifications from the lectures can be found here.


Thomas Noll