66870 - MODELLI E SISTEMI CONCORRENTI

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 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

 

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

Pre-requisiti utili, ma non strettamente necessari: linguaggi formali e automi.

Link ad altre eventuali informazioni

https://virtuale.unibo.it/course/view.php?id=25803

Orario di ricevimento

Consulta il sito web di Roberto Gorrieri