66870 - Concurrent Models and Systems

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

Assessment methods

Written and Oral examinations 

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