Inizio della pagina -
Logo DISCO
|
Visita la Versione ad elevata leggibilità
|
Vai al Contenuto della pagina
|
Vai alla Fine dei contenuti
|
Vai al Menu Principale
|
Vai alla Barra di navigazione (sei in)
|
Vai al Menu di navigazione (albero)
|
Vai alla Lista dei comandi
|
Vai alla Lista degli approfondimenti
|
Vai al Menu inferiore
|
Logo Ateneo
   
Informatica Teorica
Docente

Lucia Pomello

Data e luogo

Maggio/giugno 2011

Inizio: 30 maggio 2011

Motivazioni e obiettivi
Programma

- Modelli della concorrenza: tecniche di analisi e verifica   (6 ore circa)

(Lucia Pomello)

Verranno considerati i sistemi di transizione, il  calcolo di processi e le reti di Petri  come modelli di sistemi concorrenti  e distribuiti. Verranno introdotte e presentate le principali tecniche di analisi e verifica delle proprietà di comportamento quali: analisi strutturale, analisi dello spazio degli stati e model checking basato su ordini parziali, equivalenza all’osservazione.

 

- Tecniche di ragionamento per strutture dati infinite e processi (3 ore circa)

(Felice Cardone)

Si introducono le motivazioni e le principali applicazioni del principio di coinduzione. Queste includono la dimostrazione di correttezza di programmi che operano su stream (= liste lazy) e altre strutture dati infinite, e l'equivalenza di processi concorrenti.

 

- Teoria delle Categorie e applicazioni ai Modelli Concorrenti (6 ore circa)

(Robert F. C. Walters)

Verranno presentati gli elementi di base della teoria delle categorie mostrando in particolare le possibili applicazioni ai modelli di sistemi complessi e concorrenti.

 

- Modelli Composizionali per sistemi distribuiti probabilistici  (3 ore circa)

 (Nicoletta Sabadini)

Verranno trattati modelli basati su automi per la specifica e verifica di sistemi "complessi" distribuiti, gerarchici e probabilistici, in particolare il

il formalismo Cospan-Span(Graph), che permette di modellare reti riconfigurabili in modo composizionale. Particolare attenzione verrà dedicata alla possibilità di descrivere e verificare protocolli probabilistici.

                                                  

- Modelli di computazione e limiti fisici  (6 ore circa)

(Luca Bernardinello)

Partendo dalle considerazioni di Turing sulle caratteristiche richieste a un modello della computazione, si presentano gli studi che cercano di determinarne i limiti imposti dalle leggi della fisica. Fra i modelli alternativi a quello tradizionale, si dedica uno spazio specifico ai principi su cui si fonda la computazione quantistica.

Modalità di svolgimento

Il corso si articola in più seminari di 2/3 ore ciascuno con l’intervento anche di invitati esterni, in particolare di:

Felice Cardone, Università di Torino

Nicoletta Sabadini, Università dell’Insubria

Robert F. C. Walters, Università dell’Insubria

Modalità d’esame
Seminario finale su tema concordato
Materiale didattico

Verranno segnalati articoli e testi e verranno distribuiti lucidi, a livello indicativo si
vedano:

- C. Girault, R. Valk, Petri Nets for System Engineering, a guide to modelling,
verification and application
, Springer 2003.
- D. Sangiorgi, On the origins of Bisimulation, Coinduction, and Fixed Points, Technical
Report 2007-24, Department of Computer Science, University of Bologna, 2008

Approfondimenti

Google Translate
Translate to English Translate to French Translate to German Translate to Spanish Translate to Chinese Translate to Portuguese Translate to Arabic
Translate to Albanian Translate to Bulgarian Translate to Croatian Translate to Czech Translate to Danish Translate to Dutch Translate to Finnish Translate to Greek Translate to Hindi
Translate to Hungarian Translate to Irish Translate to Japanese Translate to Korean Translate to Norwegian Translate to Polish Translate to Romanian Translate to Russian Translate to Serbian
Translate to Slovenian Translate to Swedish Translate to Thai Translate to Turkish

(C) Copyright 2016 - Dipartimento Informatica Sistemistica e Comunicazione - Viale Sarca, 336
20126 Milano - Edificio U14
redazioneweb@disco.unimib.it - ultimo aggiornamento di questa pagina 02/05/2012