- Docente: Roberto Gorrieri
- Credits: 6
- SSD: INF/01
- Language: Italian
- Teaching Mode: In-person learning (entirely or partially)
- Campus: Bologna
- Corso: Second cycle degree programme (LM) in Computer Science (cod. 8028)
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.
- 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 text in computer science, Springer, 2015.
L. Aceto, A. Ingolfsdottir, K.G. Larsen, J. Srba
Reactive Systems:Modelling, Specification and Verification
Cambridge University Press, 2007
Assessment methods
Oral examination
Teaching tools
Lectures with the help of a beamer.
Links to further information
http://www.cs.unibo.it/~gorrieri/MSC/msc.html
Office hours
See the website of Roberto Gorrieri