- 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. 6698)
Conoscenze e abilità da conseguire
Il corso presenta metodi formali per la modellazione, l’analisi e la verifica di sistemi distribuiti utilizzando reti di Petri e altri modelli per la concorrenza. Al termine del corso, lo studente è in grado di costruire modelli di sistemi concorrenti e distribuiti, di analizzare tali modelli e di verificarne le proprietà
Contenuti
- Introduzione alla concorrenza e al problema della correttezza del progetto di sistemi reattivi.
- Reti di Petri e Sistemi di transizione etichettati.
- Linear nets. Equivalenza di linguaggio, a tracce, per isomorfismo. Bisimulazione. Logica modale BML. Process algebra Lin. Teorema di rappresentazione. Congruenza e proprietà algebriche della bisimulazione. Assiomatizzazione sound and complete.
- Forking nets. Team bisimulation. Logica modale TML. Process algebra Fork. Teorema di rappresentazione. Congruenza e proprietà algebriche della team bisimuation. Assiomatizzazione sound and complete.
- Petri nets. Place bisimulation. Structure-preserving bisimulation. Logiche modali MKL e LKL. Process algebra Pet. Teorema di rappresentazione. Congruenza e proprietà algebriche. Assiomatizzazione.
- Altre equivalenze per reti di Petri: sequenziali, concorrenti, causali.
- Bisimulazione su reti con transizioni silenti: cenni a weak e branching bisimulation.
- Il linguaggio CCS: semantica operazionale strutturata. Turing completezza di CCS finitario; indecidibilità delle equivalenze comportamentali per CCS finitario.
- Cenni a computabilità distribuita: Last man standing problem.
Testi/Bibliografia
R. Gorrieri. Syntax and Semantics of Petri Nets, Cambridge Tracts in TheoreticalComputer Science 63, CUP, 2025.
R. Gorrieri, C. Versari. Introduction to Concurrency Theory: Transition Systems and CCS, EATCS texts in theoretical computer science, Springer, 2015.
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
Agli studenti verrà assegnato un piccolo progetto, da svolgere a casa, che verrà valutato in 30-esimi. A seguire una prova scritta, anch'essa valutata in 30-esimi. Il voto finale sarà ottenuto come media di questi due voti.
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.