- Docente: Roberto Gorrieri
- Credits: 6
- SSD: INF/01
- Language: Italian
- Teaching Mode: Traditional lectures
- Campus: Bologna
- Corso: Second cycle degree programme (LM) in Computer Science (cod. 5898)
-
from Feb 19, 2025 to May 15, 2025
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.
Readings/Bibliography
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
Slidea avaialble online on the Virtuale platform
Office hours
See the website of Roberto Gorrieri
SDGs
This teaching activity contributes to the achievement of the Sustainable Development Goals of the UN 2030 Agenda.