Algebre di Processi

Il primo passo per poter studiare ed analizzare un sistema concorrente è quello di utilizzare un formalismo che permetta di costruirne il modello matematico. Un algebra di processi è una formalismo che consente di modellare sistemi concorrenti che eventualmente interagiscono tra loro.

Gli elementi di base per ottenere questo formalismo sono le azioni e gli operatori (o combinatori). Questi ultimi permettono di costruire espressioni che simulano il comportamento del sistema considerato. Con questo simbolismo si facilita la specifica e la manipolazione di processi soprattutto in un computer. Nelle algebre più utilizzate gli operatori sono in numero ristretto, ma riescono a definire gran parte delle proprietà richieste perché possono simulare molti comportamenti di un sistema.

Sono state sviluppate molte teorie algebriche di questo tipo in modo da catturare i differenti aspetti di un sistema. La prima teoria che si occupava approfonditamente di comunicazione e concorrenza è quella di Petri (Petri nets negli anni '60). Essa è una generalizzazione della teoria degli automi che permette l'occorrenza di molte azioni (transizioni tra stati) indipendenti. In particolare si fa molta attenzione al concetto di causalità tra azioni.

Il CCS (o process calculus), che analizzeremo in dettaglio più avanti, fu proposto da Milner nel 1980; poi sono state realizzate altre algebre tra cui ricordiamo Lotos, Meije, ACP e TCSP.

Abbiamo già detto che esistono vari approcci per descrivere la semantica di un'algebra di processi. Dal punto di vista operazionale, possiamo utilizzare dei grafi di transizione che descrivono i comportamenti del sistema da modellare. In particolare, i due tipi di grafi più comuni sono le Strutture di Kripke (KS) ed i Labelled Transition Systems (LTS). Nel primo caso si etichettano gli stati del grafo per descrivere in che modo sono modificati dalle transizioni; nel secondo caso, come dice il nome, le transizioni sono etichettate con azioni che causano il passaggio da uno stato all'altro.



Subsections
Morpheus 2004-02-10