Labelled Transition Systems

I sistemi di transizioni etichettate furono introdotti da Keller nel 1976 come un modello formale per descrivere programmi paralleli ed in seguito sono stati usati per dare una semantica operazionale strutturale ai linguaggi di programmazione.

I sistemi di transizione sono quindi un modello relazionale astratto basati sulle nozioni primitive di stato e transizione. Molte propietà dei sistemi concorrenti possono essere studiate tramite questa rappresentazione; bisogna essere in grado di conoscere la capacità di tali sistemi di compiere azioni appartenenti ad un insieme predeterminato Act; azioni che possono essere istantanee o durature. Ovviamente un sistema sequenziale può effettuare al più un'azione nello stesso istante, certe azioni però possono essere azioni di sincronizzazione di un processo con il sistema concorrente di cui fa parte oppure segnali inviati dal resto del sistema al processo; è ovvio che quest'ultimo tipo di azioni occorrono solamente nel caso in cui i processi cooperino. Per essere più precisi forniamo una definizione formale di Labelled Transition System (LTS).

Un LTS è una quadrupla $(Q, q_0, Act \cup\{\tau \},R)\:$ dove:

• $Q$ è un insieme di stati;
• $q_0$ è lo stato iniziale;
• $Act$ è un insieme finito e non vuoto di azioni visibili; $\tau$ è un'azione non contenuta in $Act$ ed è utilizzato per rappresentare azioni interne alla struttura.
• $R \subseteq \: Q \times (Act \cup \{\tau\}) \times Q\:$ è la relazione di transizione tale che un'elemento $(s,\alpha,r) \in R$ se esiste la possibilità di passare da uno stato s ad un altro r tramite l'azione $\alpha$.

Un LTS può essere rappresentato tramite un albero la cui radice è lo stato iniziale $q_0$ (gli stati iniziali sono rappresentati con un piccolo cerchio interno), le relazioni di transizione sono rappresentate dagli archi fra i nodi (archi etichettati con la azioni appartenenti ad $Act \cup\{\tau \}$ ), i nodi infine rappresentano gli stati appartenenti a Q.

Alcuni utili notazioni e definizioni che si riveleranno utili nel proseguio:

• Act verrà usato per denotare l'insieme delle azioni visibili; a,b,c ... denoteranno gli elementi di tale insieme;
• $Act^*$ verrà usato per denotare l'insieme delle stringhe ottenibili a partire da A; $s_1$, $s_2$, $\cdots$ rappresentano gli elementi di tale insieme e $\varepsilon$ la stringa vuota.
• $Act_\tau$ verrà usato per denotare le azioni appartenenti ad $Act \cup\{\tau \}$

Definizione 2..1   Negli LTS, un cammino (o computazione) $\pi$ è una sequenza $(q_0, \alpha_0,q_1)$ $(q_1,\alpha_1,q_2)$ $(q_2,\alpha_2,q_3)\cdots$ dove ogni tripla $(q_i,\alpha_i, q_{i+1}) \in R$. Un cammino può essere finito o infinito (in base al numero di transizioni che contiene) ed eventualmente può avere dei cicli al suo interno; possiamo inoltre trovare cammini nulli rappresentati da un sequenza vuota.

Negli LTS le transizioni tra stati sono etichettate con azioni che possono essere visibili o invisibili, perciò è importante introdurre il significato ed il comportamento che assume un'azione all'interno di un sistema.

Quindi un Labeled Transition System è sostanzialmente un automa non deterministico. Nella teoria degli automi, un automa è rappresentato dal linguaggio che riconosce ed esso è equivalente ad un altro se e solo se i linguaggi accettati da essi sono uguali. Questo modo di determinare l'equivalenza crea problemi se si stanno trattando sistemi non-deterministici; perciò si inserisce la nozione di bisimulazione che permette di distinguere processi con lo stesso "linguaggio", ma comportamenti diversi.

Esempio Bill-Ben 1: Vediamo adesso un semplice esempio di LTS formato da 5 stati (di cui uno iniziale), 3 azioni e 5 transizioni:

Dal nodo iniziale $q_0$ escono due archi distinti (transizioni $(q_0,play,$ $q_1)$ e $(q_0,work,q_2)\:$) che raggiungono due stati differenti $q_1$ e $q_2$. Da questi si raggiunge sempre $q_3$ che ha un solo arco uscente (transizione $(q_3,\tau,q_4)\:$) con il quale si raggiunge il nodo finale $q_4$.