Date: Wed 7 Feb
Time: 16.00
Place: room 214

Speaker: Rosario Pugliese (Univ. di Roma)
Title: Teorie semantiche per algebre di processo asincrone
Reference: Catuscia Palamidessi

Abstract. La maggior parte delle algebre di processo studiate in letteratura si basa su un meccanismo di comunicazione sincrona e, salvo poche eccezioni, non prevede lo scambio di dati durante la comunicazione tra processi. Tuttavia, esistono sistemi concorrenti e distribuiti la cui descrizione risulta piu' naturale se si adotta un linguaggio con comunicazione asincrona. In questo seminario presenteremo teorie semantiche basate sul concetto di testing per due algebre di processo che adottano meccanismi di comunicazione asincrona. La prima algebra di processo considerata e' una variante di TCCS (sostanzialmente CCS con operatori di scelta nondeterministica interna ed esterna) con comunicazioni senza scambio di valori. La seconda realizza la comunicazione di valori ed adotta il paradigma di comunicazione di Linda (pattern-matching su tuple). Essa e' ottenuta sostituendo le primitive di comunicazione della variante di TCCS considerata in precedenza con le primitive Linda per il coordinamento di attivita' concorrenti. In questo caso la comunicazione avviene tramite uno spazio dati condiviso, lo Spazio delle Tuple, senza uso di canali. Per ciascuna delle due algebre di processo presenteremo una semantica comportamentale definita su due livelli. Quello piu' dettagliato associa ai processi un Sistema di Transizione Etichettato e descrive il loro comportamento operazionale. Tale semantica e' definita senza far uso di componenti passive (output e tuple sono realizzati come processi), evitando cosi' di introdurre una nozione di "stato". Il secondo livello astrae dai dettagli ritenuti irrilevanti e fornisce una descrizione osservazionale del comportamento dei processi. Esso e' costituito da una relazione di preordine sui processi basata sul concetto di testing. Inoltre, per entrambe le algebre di processo considerate, presenteremo due caratterizzazioni equivalenti del preordine comportamentale: una equazionale (utile per provare relazioni tra processi mediante semplice manipolazione sintattica) ed una denotazionale (la quale fornisce una interpretazione dei processi come oggetti di un dominio matematico con particolari proprieta').