66870 - MODELLI E SISTEMI CONCORRENTI

Anno Accademico 2024/2025

  • Docente: Roberto Gorrieri
  • Crediti formativi: 6
  • SSD: INF/01
  • Lingua di insegnamento: Italiano
  • Modalità didattica: Convenzionale - Lezioni in presenza
  • Campus: Bologna
  • Corso: Laurea Magistrale in Informatica (cod. 5898)

Conoscenze e abilità da conseguire

Al termine del corso, lo studente conosce i paradigmi di base della concorrenza, i loro modelli ed i sistemi di verifica di proprietà di tali modelli. È in grado di analizzare semplici programmi concorrenti con strumenti automatici o semi-automatici.

Contenuti

- Introduzione alla concorrenza e al problema della correttezza del progetto di sistemi reattivi.

- Sistemi di transizione etichettati.

- Equivalenze comportamentali: tracce, simulazione, bisimulazione forte e debole, proprietà.

- Il linguaggio CCS: semantica operazionale strutturata.

- Sottoclassi di CCS: processi finiti, processi a stati finiti, processi regolari, BPP, processi a rete finita, CCS finitario.

- Turing completezza di CCS finitario; indecidibilità delle equivalenze comportamentali per CCS finitario.

- Cenni a CCS value-passing.

- Proprieta' algebriche, congruenze comportamentali e cenni alle assiomatizzazioni.

- Espressività di CCS: implementabilità di operatori aggiuntivi (scelta interna, hiding, composizione sequenziale)

- Problema della sincronizzazione muti-way: Multi-CCS; caso di studio: filosofi a cena.

- Reti di Petri: definizione, equivalenze comportamentali, proprietà decidibili, espressività.

- Cenni ai linguaggi per rappresentare reti di Petri. Computabilità distribuita.

- Teoria del punto fisso, minimi e massimi punti fissi, equivalenza forte come massimo punto fisso.

- Logica di Hennessy-Milner (HML), estensione con formule definite in modo ricorsivo, modal mu-calculus.

- Tool di analisi e verifica per CCS e HML: Concurrency Workbench (CWB).

- Modellazione, analisi e verifica di alcuni algoritmi di mutua esclusione con CWB.

Testi/Bibliografia

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 VerificationCambridge University Press, 2007

R. Gorrieri

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

Metodi didattici

Lezioni frontali con proiettore

Modalità di verifica e valutazione dell'apprendimento

Prova scritta da svolgere a casa ed orale

Strumenti a supporto della didattica

Slide disponibili su virtuale

Orario di ricevimento

Consulta il sito web di Roberto Gorrieri

SDGs

Istruzione di qualità Parità di genere Lavoro dignitoso e crescita economica

L'insegnamento contribuisce al perseguimento degli Obiettivi di Sviluppo Sostenibile dell'Agenda 2030 dell'ONU.