- 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
L'insegnamento contribuisce al perseguimento degli Obiettivi di Sviluppo Sostenibile dell'Agenda 2030 dell'ONU.