- 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. 6698)
Learning outcomes
The course is about formal methods for the modelling, analysis and verification of distributed systems, by using Petri nets and other concurrency models. At the end of the course, the student is able to build models of concurrent and distributed systems, to analyze such models and to verify their properties.
Course contents
- Introduction to concurrency and to the problem of the correctness of reactive systems design.
- Petri nets and labeled transition systems
- Linear nets. Language equivalence, trace equivalence, isomorphism equivalence. Bisimulation. Modal logic BML. Process algebra Lin. Representability theorem. Congruence and algebraic properties of bisimulation. Sound and complete axiomatization.
- Forking nets. Team bisimulation. Modal logic TML. Process algebra Fork. Representability theorem. Congruence and algebraic properties of team bisimuation. Sound and complete axiomatization.
- Petri nets. Place bisimulation. Structure-preserving bisimulation. Modal logics MKL and LKL. Process algebra Pet. Representability theorem. Congruence and algebraic properties. Axiomatization.
- Other equivalences for Petri nets: sequential, concurrent, causal.
- Bisimulation on linear nets with silent transitions: weak and branching bisimulation.
- The language CCS: syntax and SOS semantics. Turing completeness of finitary CCS; undecidability of behavioral equivalences of finitary CCS.
- Distributed computability: Last man standing problem.
Readings/Bibliography
R. Gorrieri. Syntax and Semantics of Petri Nets, Cambridge Tracts in TheoreticalComputer Science 63, CUP, 2025.
R. Gorrieri, C. Versari. Introduction to Concurrency Theory: Transition Systems and CCS, EATCS texts in theoretical computer science, Springer, 2015.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
Small-size home-project, to be evaluated up to 30, and then an oral examination, to be evaluated up to 30. The final grade is computed as the average of these two grades.
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.