Obiettivi formativi

L'obiettivo del corso e' quello di fornire i concetti e principi fondamentali che sono alla base di una corretta programmazione concorrente, con o senza mobilita' di codice. A tal scopo verranno considerati dei modelli algebrici, vale a dire dei linguaggi molto semplici, che racchiudono tutte le caratteristiche principali dei linguaggi concorrenti reali. Tali modelli, chiamati calcoli di processo(quali CCS, Pi-calcolo, Mobile Ambient), essendo piu semplici dei linguaggi reali, ben si prestano allo studio delle problematiche tipiche della concorrenza. Durante il corso verrano forniti vari esempi ed applicazioni. Nell'ultima parte del corso verrano accennati nozioni di linguaggi distribuiti, in cui agenti concorrenti migrano all'interno di reti di calcolatori.

Programma

-Definizione di sistemi trasformazionali, reattivi, concorrenti e distribuiti
-Sistemi reattivi e richiami di teoria degli automi
-Semantica operazionale per sistemi reattivi: Sistema a transizioni etichettate
-Semantica comportamentale per sistemi reattivi: bisimulazione forte
-Processi sequenziali: sintassi, semantica operazionale, bisimulazione
-Processi concorrenti (CCS): sintassi, semantica operazionale, bisimulazione
-Esempi di sistemi concorrenti in CCS
-Bisimulazione debole
-Tecniche di prova di equivalenza tra processi
-Specifica e verifica di proprieta': Hennessy-Milner Logic
-Sistemi Mobili
-Pi-calcolo: sintassi e semantica operaizionale
-Esempi di sistemi mobili in pi-calcolo
-Bisimulazione forte e debole in pi-calcolo
-Accenni di modelli concorrenti e distribuiti.

Modalità d'esame

Il candidato dovra' sostenere una prova scritta. Voti minori o uguali a 26 possono essere confermati. Per voti dal 27 in su' e' richiesto un colloquio orale con il docente.