66870 - Concurrent Models and Systems

Course Unit Page

  • Teacher Roberto Gorrieri

  • Credits 6

  • SSD INF/01

  • Teaching Mode Traditional lectures

  • Language Italian

  • Campus of Bologna

  • Degree Programme Second cycle degree programme (LM) in Computer Science (cod. 8028)

  • Teaching resources on Virtuale


This teaching activity contributes to the achievement of the Sustainable Development Goals of the UN 2030 Agenda.

Gender equality Decent work and economic growth Reduced inequalities

Academic Year 2021/2022

Learning outcomes

At the end of the course, the student will learn the basic ingredients of concurrency theory, their models and verification systems on such models. (S)He will be able to analyze simple concurrent programs with automatic or semi-automatic tools.

Course contents

- Introduction to concurrency and to the problem of the correctness of reactive systems design.

- Labeled transition systems

- Behavioral equivalences: traces, simulation, bisimulation f(strong and weak), properties.

- The language CCS: syntax and SOS semantics.

- Subclasses of CCS: finite processes, finite-state processes, regular processes, BPP, finite-net processes, finitary CCS.

- Turing completeness of finitary CCS; undecidability of behavioral equivalences of finitary CCS.

- Value-passing CCS.

- Algebraic properties, behavioral congruences and axiomatizations.

- Espressivieness of CCS: encodability of additional operators (internal choice, hiding, sequential composition) 

- The problem of muti-way synchronization: Multi-CCS; case study: dining philosophers.

- Petri nets: definition, equivalences, decidable properties, expressiveness.

- Languages for representing Petri nets. Distributed computability.

- Fixpoint theory, least and greates fixpoints, strong bisimilarity as a greatest fixpoint.

- Hennessy-Milner Logic (HML), estention with recursively defined formulae, modal mu-calculus.

- Analysis and verification tools for CCS and HML: Concurrency Workbench (CWB).

- Modeling, analysis and verification of some mutual exclusion algorithms with CWB.


R. Gorrieri, C. Versari

Introduction to Concurrency Theory: Transition Systems and CCS

EATCS texts in theoretical computer science, Springer, 2015.


L. Aceto, A. Ingolfsdottir, K.G. Larsen, J. Srba

Reactive Systems: Modelling, Specification and Verification

Cambridge University Press, 2007


R. Gorrieri

Process Algebras for Petri Nets: The Alphabetization of Distributed Systems, EATCS monographs in theoretical computer science, Springer, 2017

Teaching methods

Lectures with the help of a beamer.

Assessment methods

Little home-project and oral examination.

Teaching tools

Prior knowledge about formal languages and automata is useful, but not strictly necessary.

Links to further information


Office hours

See the website of Roberto Gorrieri