Regular Expressions

Lezione del 2018-11-08.

Le espressioni regolari (vedi [SAKH2019a]) definiscono un linguaggio formale come un insieme di stringhe su un alfabeto finito di simboli.

Più in particolare, le espressioni regolari definiscono una grammatica (vedi [SLKU1995] pag.2) di tipo context free ([SLKU1995] pag.3)

La seguente

\[\mathcal{L} := 0 \vert 1 \vert a \vert e_1 + e_2 \vert e_1 \cdot e_2 | e^*\]

definisce il linguaggio formale \(\mathcal{L}\).

Da un punto di vista insiemistico, l’espressione regolare e definisce un insieme di parole L, sottoinsieme di tutte le possibili parole che si possono formare con l’alfabeto Alph: \(e \mapsto L \subseteq Alph^* \quad Alph = \{a, b, c, \cdots \}\)

In denotational semantics, ponendo a sinistra la regular expression e a destra il suo significato, inteso come set di parole, ottenuto per induzione. Abbiamo le seguenti:

• \([\![ 0 ]\!] = \text{empty set of words: } \emptyset\) ;

• \([\![ 1 ]\!] = \text{set che contiene una sola stringa, la stringa vuota: } \{\lambda\}\) ;

• \([\![ a ]\!] = \text{insieme di stringhe che contengono un solo elemento: } \{a\} \\ \, \text{con} \, a \, \text{elemento dell'alfabeto:} \, a \in Alph \, \text{;}\)

• plus operator: \([\![ e_1 + e_2 ]\!] = [\![ e_1 ]\!] \cup [\![ e_2 ]\!]\);

  dove l’unione di due insiemi è espressa da \(L_1 \cup L_2 = \{u \vert u \in L_1 \vee u \in L_2\}\) ; \(L_1\) è il linguaggio (ovvero le parole) generato dall’espressione regolare \(e_1\), mentre \(L_2\) è il linguaggio generato dall’espressione \(e_2\).

• concatenation operator: \([\![ e_1 \cdot e_2 ]\!] = [\![ e_1 ]\!] \cdot [\![ e_2 ]\!]\) ;

  dove la concatenazione tra insiemi è formata dalle stringhe ottenute concatenando gli elementi dei due insiemi: \(L_1 \cdot L_2 = \{u \, v \vert u \in L_1 \wedge v \in L_2\}\) ;

  composizione sequenziale (sequential composition) è un sinonimo dell’operatore di concatenazione;

  attenzione all’ordine degli argomenti, questo operatore non ha la proprietà simmetrica;

• Kleene's operator (or Kleene’s star) : \([\![ e^* ]\!] = ( [\![ e ]\!] )^*\) ;

  osserviamo che è una Kleene’s closure del corpo dell’espressione;

  la stella denota iterazione; similmente ad un while ma senza il test booleano: \(L \subseteq (Alph)^* \quad L^* = \bigcup_{i \geq 0} L^i = L^0 \cup L^1 \cup L^2 \ \dots\) ; dove \(L^i = L \cdot L \cdot \dots L \quad \text{i times}\) ;

  volendo definire \(L^i\) per induzione:

  \[\begin{split}L^i = \begin{cases} \{\lambda\} & \text{se } i = 0 \\ L \cdot L^{i-1} & \text{se } i > 0 \end{cases}\end{split}\]

  ovvero: per i=0 è il set con la stringa vuota, per i>0 è la concatenazione di L con L di i-1.

  Si nota che la stringa vuota é sempre inclusa. Per analogia con il while potremmo dire che si considera l’eventualità di saltare il loop.

Le espressioni regolari sono finite, complete e decidibili. Inoltre Kleene ha dimostrato che possono generare automi finiti non deterministici (detti NDFA: non deterministic finite automata).

Sempre Kleene, inoltre, nel 1956 dimostrò l’equivanza (kleene equivalence) tra automi finiti non deterministici e automi finiti deterministici (detti DFA: deterministic finite automaton).

In tal modo si osservano le relazioni espresse nel seguente diagramma:

Nel diagramma si nota il riferimento alle grammatiche regolari [1].

Queste equivalenze sono estremamente utili. Perché quando si progetta un nuovo linguaggio, l’insieme di parole chiave, costanti, valori, possono formare un insieme infinito di elementi. D’altro canto abbiamo bisogno di un modo finito per esprimere il linguaggio. E l’uso delle espressioni regolari per la definizione del linguaggio è uno strumento finito in grado di generare insiemi infiniti [2].

A questo punto nasce la necessità di leggere con un computer le stringhe scritte (ovvero i programmi) tramite un analizzatore lessicografico in grado di verificare che le stringhe siano corrette.

Per fare ciò si esegue la procedura mostrata nel precedente diagramma:

• date le regular expressions;
• si costruisce al volo il relativo NDFA;
• si trasforma con apposito algoritmo il NDFA in DFA;
• si implementa il DFA, che essendo finito e deterministico è decidibile;
• si sottopongono al DFA le stringhe da analizzare per vedere se sono accettabili dall’automa.

Attenzione al fatto che siamo a livello lessicografico. Ovvero prima del controllo sintattico. Questo viene dopo: per l’analisi sintattica le espressioni regolari non sono sufficienti, sevono tool più potenti.

Altro aspetto cui fare attenzione, è il fatto che abbiamo parlato di analisi di linguaggi. Diverso è il caso se vogliano utilizzare le espressioni regolari per analizzare sistemi reattivi o concorrenti. In questo caso è necessario utilizzare nozioni di equivalenza diversi.

regular expressions examples

• \([\![ a \cdot b ]\!] = \{ab\}\);
• \([\![ a^* \cdot ( 0 + 1 + 2 + \cdots 9 )^* ]\!] = \{ \lambda, \cdots, a, aa, \cdots a0, a00, \cdots, aa11, \cdots, a11, \cdots \}\);
• \([\![ a^* ]\!] = \{ \lambda, a, aa, aaa, \cdots \}\);
• nota: \(a^+ = a^* - \{ \lambda \}\);

R.E. trace Equivalence

Osservando le seguenti:

• \([\![ e_1 ]\!] = [\![ a \cdot ( b + c ) ]\!] = \cdots\) :

  \[\begin{split}\cdots & [\![ a ]\!] \cdot [\![ b + c ]\!] = \\ & \{a\} \cdot ([\![ b ]\!] \cup [\![ c ]\!]) = \\ & \{a\} \cdot (\{b\} \cup \{c\}) = \\ & \{a\} \cdot \{ b, c \} = \{ab, ac\}\end{split}\]

• \([\![ e_2 ]\!] = [\![ a b + a c ]\!] = \cdots\) :

  \[\begin{split}\cdots & [\![ a b ]\!] \cup [\![ a c ]\!] = \\ & [\![ a ]\!] \cdot [\![ b ]\!] \cup [\![ a ]\!] \cdot [\![ c ]\!] = \\ & \{ a \} \cdot \{ b \} \cup \{ a \} \cdot \{ c \} = \\ & \{ a b \} \cup \{ a c \} = \{ab, ac\}`;\end{split}\]

si nota che la semantica è la stessa, ma le due sintassi sono diverse. Capita spesso.

I seguenti alberi illustrano l’interpretazione sintattica delle due formule predette:

Quindi \(e_1\) e \(e_2\) sono trace equivalent (o language equivalent) se e solo se denotano la stessa grammatica:

\[e_1 = e_2 \iff [\![e_1]\!] = [\![e_2]\!]\]

ovvero generano lo stesso linguaggio [3]. Questa è una vera equivalenza algebrica, infatti valgono le proprietà riflessiva, simmetrica e transitiva.

Ma attenzione alla decidibilità. Le equivalenze di espressioni regolari sono decidibili perché le regular expressions sono meno espressive della macchina di Touring. Invece l’equivalenza nei linguaggi di programmazione in generale non è decidibile. Questo perché i linguaggi sequenziali sono equivalenti a macchine di Touring. E in queste in generale non è possibile decidere se due programmi sono equivalenti.

Vale anche l’osservazione che le espressioni regolari definiscono linguaggi di specifiche. Inoltre sono sufficienti per definire i token nei linguaggi di programmazione.

Dal fatto che esiste il concetto di (trace) equivalenza per le espressioni regolari segue che è possibile avere un algoritmo che può dirci se due espressioni regolari in input sono equivalenti o no, ovvero se generano lo stesso linguaggio.

lezione del 2018-11-09

L’applicazione del concetto di equivalenza all’insieme di tutte le espressioni regolari, permette di suddividerle in classi di equivalenza. Ogni classe di equivalenza ospita i termini equivalenti.

R.E. Axiomatic Equivalence

E' possibile usare un insieme di assiomi e regole di inferenza per definire l’equivalenza di regular expressions.

Abbiamo:

• idempotenza \(X + X = X\)

• commutativa \(X + Y = Y + X\)

• associativa a sinistra \((X + Y) + Z = X + (Y + Z)\)

• esistenza dello zero [4]

  \[\begin{split}& x + 0 = x \\ & 0 + x = x \\ & x \cdot 0 = 0 \\ & 0 \cdot x = 0\end{split}\]

• esistenza dell’uno

  \[\begin{split}& x \cdot 1 = x \\ & 1 \cdot x = x\end{split}\]

• distributiva della sequencial composition rispetto il +:

  \[\begin{split}& X \cdot (Y + Z) = X \cdot Y + X \cdot Z \\ & (X + Y) \cdot Z = X \cdot Z + Y \cdot Z\end{split}\]

• kleene’s star: \(X^* = 1 + X \cdot X^*\)

  Nota. Applicando la precedente:

  \[\begin{split}0^* & = 1 + 0 \cdot 0^* \\ & = 1 + 0 \\ & = 1\end{split}\]

Nota

Non esiste la proprietà commutativa per la sequential composition, perché per questa operazione l’ordine dei termini è significativo.

Nota

E' possibile provare la idempotenza provando che \(X + X\) e \(X\) hanno la stessa semantica, ovvero:

\[\begin{split}& \text{tesi: } [\![ X + X ]\!] = [\![ X ]\!] \\ & \text{vale: } [\![ X + X ]\!] = [\![ X ]\!] \cup [\![ X ]\!] \\ & \text{insiemisticamente: } [\![ X ]\!] \cup [\![ X ]\!] = [\![ X ]\!]\end{split}\]

da cui la tesi. In pratica \([\![ X ]\!] \cup [\![ X ]\!]\) indica l’unione di un linguaggio (un insieme) con se stesso: questa operazione restituisce il linguaggio stesso.

E' interessante osservare che la \(0^* = 1\) permette di semplificare la sintassi delle espressioni regolari eliminando l’1:

\[\mathcal{L} := 0 \vert a \vert e_1 + e_2 \vert e_1 \cdot e_2 | e^*\]

quindi la semantica delle espressioni regolari è tale da semplificare la sintassi.

Esiste un teorema che enuncia: date due espressioni regolari, queste sono trace equivalent se e solo se i due termini possono essere resi equivalenti applicando gli assiomi:

\[\forall e_1, e_2 \in E \quad e_1 =_{te} e_2 \iff e_1 =_{A} e_2\]

dove E è l’insieme delle espressioni regolari, \(=_{te}\) indica trace equivalence, ovvero \([\![ e_1 ]\!] = [\![ e_2 ]\!]\), mentre \(=_{A}\) indica equivalenza secondo gli assiomi precedentemente indicati.

Una equivalenza secondo gli assiomi si prova partendo dall’espressione \(e_1\), e applicando a questa gli assiomi presentati in precedenza, fino a trasformarla, se si riesce, nell’espressione \(e_2\).

Il teorema in osservazione afferma che la trace equivalence e la axiomatic equivalence generano le stesse classi di equivalenza: suddividono l’insieme E nelle stesse partizioni.

La proposizione se e solo se del precedente teorema, significa che valgono:

• sia \(e_1 =_{te} e_2 \Leftarrow e_1 =_{A} e_2\);
• che \(e_1 =_{te} e_2 \Rightarrow e_1 =_{A} e_2\).

La prima relazione afferma che due espressioni regolari assiomaticamente equivalenti, implicano l’equivalenza semantica. Questa è detta correctness (o soundness).

Considerando la seconda relazione, ovvero l’equivalenza semantica implica quella assiomatica, è detta completeness.

Kleene nel 1956 fu in grado di provare solo il soundness. La completeness fu provata nel 1999 da Dexter Kozen, utilizzando l’univocità dell’automa minimo per \(e_1, e_2\): dato l’automa minimo, Kozen lo utilizzò per dimostrare gli assiomi.

Il teorema predetto vale per le espressioni regolari come generatori di linguaggi. Per il tema più generale dell’uso delle espressioni regolari per i sistemi concorrenti, il teorema predetto ancora non è completamente dimostrato. E' stato dimostrato per una sintassi semplificata. Quindi vi è il sospetto che gli assiomi non siano sufficienti per definire l’equivalenza per sistemi concorrenti rappresentabili con la sintassi completa delle espressioni regolari.

Nota

Mentre da un punto di vista matematico l’equivalenza semantica e quella assiomatica possono essere interpretate come due modi diversi di esprimere lo stesso concetto di equivalenza, da un punto di vista della computer scienze, sono due interpretazioni diverse dell’informazione: una (la semantica) orientata all’algoritmo, l’altra alla sintassi.

Non deterministic interpretation of R.E.: intuition

lezione del 2018-11-15

Riprendiamo la sintassi delle espressioni regolari:

\[\begin{split}& Alph = \{a, b, c, \cdots \} \\ & \mathcal{L} ::= 0 \vert 1 \vert a \vert e_1 + e_2 \vert e_1 \cdot e_2 | e^*\end{split}\]

Consideriamo l’alfabeto come astrazioni di azioni. Ad esempio: send, receive, input, output, …

E interpretiamo le espressioni regolari come descrizioni di sistemi reattivi. Ovvero sistemi che reagiscono alle condizioni esterne: sempre attivi, eseguono i comandi senza terminare, ma rimangono in attesa del prossimo comando da eseguire.

Nota

In questa sintassi, per ora manca l’operatore di parallel composition.

Gli operatori mostrati possono essere interpretati informalmente come segue.

Avvertimento

La terminologia può ingannare. Questi sono sistemi elementari. Considera che in inglese operator si traduce con il termine italiano operatore, intendendo una persona o una cosa che esegue compiti, verosimilmente in modo continuativo.

Quindi, attenzione a non confondere il concetto di operatore, che in italiano assume anche il significato di simbolo che esprime una operazione. Gli anglosassoni per questo significato utilizzano spesso il termine operation.

• 0 è un unsuccesfull terminal operator ovvero un sistema che ha concluso l’attività senza successo.

• 1 è un successfull terminal operator: un sistema che ha concluso l’attività con successo.

  Quindi sia l'1 che lo 0 indicano uno stop dell’attività, ma con diversi significati: soddisfacimento, o meno, della richiesta.

• a é un sistema che può eseguire l’azione a e poi terminare con successo. Notiamo che la terminazione con successo è successiva alla esecuzione dell’azione a.

• \(e_1 + e_2\) è la non deterministic composition. Un sistema in grado di eseguire le azioni \(e_1\) oppure quelle \(e_2\). E' una scelta tra \(e_1\) ed \(e_2\), ma non condizionata da un test booleano. La scelta se eseguire l’una o l’altra è determinata dall’ambiente esterno. Alcune volte l’ambiente richiederà \(e_1\), altre volte \(e_2\). E quando è stata fatta la scelta, l’alternativa non è più possibile, viene eliminata fino al prossimo run.

  I sistemi paralleli hanno sempre un comportamento di questo tipo, esplicito o implicito. Si immagini un gruppo di sistemi, ognuno in grado di eseguire alcune attività. Ogni sistema elabora autonomamente, salvo comunicare ogni tanto con un altro sistema del gruppo.

• \(e_1 \cdot e_2\) è la sequential composition. Un sistema in grado di eseguire le azioni \(e_1\) e, quando queste sono pronte a terminare con successo, il controllo passa a \(e_2\). Quindi fornisce un ordine: prima \(e_1\) e poi \(e_2\), ma solo se \(e_1\) è terminato con successo.

  La sequencial composition è sempre presente, in ogni linguaggio di specifiche. Questo perché ogni algoritmo ha necessità di indicare un ordine delle operazioni da effettuare.

• \(e^* = 1 + e \cdot e^*\) è simile ad un sistema ricorsivo. In pratica è un sistema non deterministic composition che può decidere di terminare immediatamente con successo (salta il corpo del processo), oppure eseguire il processo e, se non fallisce, decidere di ripartire nuovamente.

  Il seguente è un diagramma descrittivo di un sistema \(e^*\):

  

Nel complesso le espressioni regolari sono un linguaggio di descrizione di sistemi reattivi piuttosto completo. Manca la parallel composition, che può essere in qualche modo simulata tramite comportamenti paralleli.

Manca anche la possibilità di specificare il tempo e la localizzazione: vengono descritti solo gli aspetti funzionali.

D’altro canto permettono di esprimere la non deterministic composition tramite l’operatore \(e_1 + e_2\), e questo è un concetto fondamentale nella programmazione parallela. Ad esempio se si hanno due processi che effettuano assegnazioni diverse in una variabile, quale dei due vince lasciando il proprio valore nella variabile al termine del run, dipende da una serie di fattori non controllabili: temperatura, presenza di altri processi, frequenza del clock, cache, … Quindi eseguendo più test avremo risultati diversi: alcune volte vincerà il primo processo, altre volte vincerà il secondo.

Non deterministic interpretation of R.E: semantics

Per l’interpretazione classica delle R.E. abbiamo usato la denotation semantics perché ci ha permesso di concentraci sugli stati iniziali e finali.

Ora, avendo a che fare con processi concorrenti, limitare l’analisi ai soli stati iniziali e finali non è più sufficiente. Per questo motivo si usa una structural operational semantics che permette di spiegare il comportamento del sistema passo per passo.

Per comprendere il motivo di questa necessità, si riprendano i sistemi illustrati qui di seguito.

Se ci limitiamo ad osservare funzionalmente le sequenze di azioni che i due sistemi sono in grado di eseguire (ovvero le loro trace), sappiamo che sono equivalenti: soddisfano il criterio di trace equivalence. Entrambi sono in grado di eseguire sequenze del tipo ab oppure ac.

Ma considerandoli sistemi reattivi, supponiamo che:

• l’azione a sia una read, quindi una sincronizzazione con un sistema esterno che alimenta un dato in lettura,
• l’azione b sia una stampa del dato ricevuto su un device (printer1);
• l’azione c sia una stampa del dato ricevuto su un secondo device (printer2).

Questo è uno scenario molto comune. Un processo solitamente dispone di più canali di uscita, e un dato può essere emesso su uno di questi canali a richiesta dell’ambiente.

In questo scenario il processo a sinistra (\(e_1\)) legge il dato (azione a) e poi l’utente sceglie se stamparlo su printer1 oppure su printer2.

Invece il processo a destra (\(e_2\)) l’utente deve decidere subito su quale printer scrivere perché deve iniettare la sequenza ab oppure la sequenza ac. Non può decidere se b o c dopo la lettura del dato (a).

Questo punto é molto importante.

Premesso che potremo considerare i due sistemi equivalenti se si comportano nello stesso modo quando inseriti nello stesso ambiente.

Quindi immaginiamo un test dei due sistemi \(e_1\) ed \(e_2\) in un ambiente formato con un ulteriore sistema in grado di alimentarli con il dato da stampare, ad esempio la sequenza \(\bar{a} \cdot \bar{b} \cdot 1\), dove \(\bar{a}\) e \(\bar{b}\) sono i segnali di sincronizzazione con i relativi comandi, mentre 1 indica terminazione con successo.

Il comportamento di \(e_1\) è mostrato qui sotto:

Nel diagramma precedente ogni riquadro rappresenta a sinistra il sistema \(e_1\) e a destra, in parallelo, il sistema che lo alimenta.

• Al primo comando di sincronizzazione (\(\bar{a}\): step 1) il sistema \(e_1\) raggiunge il nodo di branch e si pone in attesa del comando successivo. In parallelo l’alimentatore raggiunge lo stato \(\bar{b} \cdot 1\).
• Al secondo comando di sincronizzazione (\(\bar{b}\): step 2) il sistema \(e_1\) raggiunge il nodo di terminazione con successo. In parallelo anche l’alimentatore raggiunge lo stato 1. Quindi tutto ok.

Vediamo ora i comportamenti possibili di \(e_2\); sono mostrati qui di seguito:

In questo diagramma, come nel precedente, ogni riquadro rappresenta a sinistra il sistema in osservazione (qui è \(e_2\)) e a destra, in parallelo, il sistema che lo alimenta.

Inoltre qui abbiamo due colonne: una per ogni possibile comportamento di \(e_2\).

Consideriamo la colonna sinistra.

• Al primo comando di sincronizzazione (\(\bar{a}\): step 1 nella colonna sinistra) il sistema \(e_2\) prende il ramo a sinistra e si pone in attesa del comando successivo. In parallelo l’alimentatore raggiunge lo stato \(\bar{b} \cdot 1\).
• Al secondo comando di sincronizzazione (\(\bar{b}\): step 2 della colonna sinistra) il sistema \(e_2\) raggiunge il nodo di terminazione con successo. In parallelo anche l’alimentatore raggiunge lo stato 1. Qui è ok.

Ma è possibile anche il comportamento descritto nella colonna a destra.

• Al primo comando di sincronizzazione (\(\bar{a}\): step 1 nella colonna destra) il sistema \(e_2\) prende il ramo a destra e si pone in attesa del comando successivo. In parallelo l’alimentatore raggiunge lo stato \(\bar{b} \cdot 1\).
• Dopo di che, siamo in una situazione di stallo (deadlock state). Perché il sistema \(e_2\) è pronto a ricevere il comando c, mentre il sistema di alimentazione deve inviare un comando b. Questo non va bene.

La presenza di possibili deadlock è un problema tipico dei sistemi distribuiti/paralleli. É necessario evitarli accuratamente, e vanno scoperti nelle prime fasi di progettazione, perché correggerli dopo l’implementazione del sistema può essere estremamente oneroso [5].

D’altro canto un sistema distribuito può essere formato da centinaia, o migliaia di componenti. In queste condizione una analisi manuale non è possibile. É necessario utilizzare tool automatici di analisi, che verifichino il comportamento di tutto il sistema all’accadere di tutte le possibili condizioni. E per fare questo devono considerare la struttura di branching dei diversi componenti.

Quindi non possiamo usare l’equivalenza linguistica per effettuare questo tipo di verifiche.

Per lo stesso motivo non è possibile utilizzare un approccio puramente funzionale. Perché anche le funzioni si concentrano su due soli punti nevralgici: l’input alla funzione e il suo output.

lezione del 2018-11-29

Il fenomeno del deadlock è stato illustrato con il problema dei filosofi a cena nel 1965 da E. Dijkstra. Si supponga di avere un gruppo di filosofi, che non possono parlare tra loro, seduto ad un tavolo rotondo. Ogni filosofo ha a disposizione una forchetta, ma per mangiare deve avere in mano due forchette. Quindi potrà mangiare solo se il suo compagno a lato gli lascia usare la sua forchetta. Il dedloack avviene se tutti i filosofi decidono di mangiare e prendono la propria forchetta, senza lasciarla a disposizione del vicino.

Nota: ci concentriamo su linguaggi di specifiche con handshacking (messagge passing between processes). Ma gli stessi ragionamenti si possono applicare a linguaggi di specifica che utilizzano memorie condivise per effettuare la sincronizzazione. Quindi l’approccio input/output non è l’unico usabile.

Consideriamo il seguente diagramma. Abbiamo sia a destra che a sinistra un sistema che risponde al comando a e termina con successo.

A sinistra il sistema \(A_1\) è deterministico, invece a destra \(A_2\) ha un comportamento non deterministico. Dall’esterno non possiamo eseguire un test che ci permetta di capire con quale di questi due abbiamo a che fare, e il comportamento appare sempre del tutto equivalente. Possiamo pensare di semplificare il progetto sostituendo il sistema \(A_2\) con il sistema \(A_1\).

In generale avremo il seguente processo.

Dato un programma scritto in un linguaggio di specifica che supporti il non determinismo, lo traduciamo in un automa con transizioni:

\[P_1 \rightsquigarrow A_1\]

Quindi possiamo avere, ad esempio, un programma scritto con la sintassi delle espressioni regolari, modellato tramite un automa che rappresenta un labeled transition system[6]. L’automa in questione solitamente è dotato di un numero elevatissimo di stati e transizioni, al limite anche infinito. Perciò il passo successivo consiste nel trasformate l’automa in una versione equivalente, possibilmente più piccola e con numero finito di stati:

\[P_1 \rightsquigarrow A_1 \rightsquigarrow A_2\]

La trasformazione verso un automa più piccolo avviene utilizzando relazioni di equivalenza, che sono divise in due classi:

• testing equivalences;
• bisimulation equivalences.

Le equivalenza tramite test utilizzano le attività di test per definire l’equivalenza tra automi diversi (model checking). In questo ambito, a causa del fatto che il non determinismo del sistema può generare automi a stati infiniti, i test possono (e devono) essere rappresentati con formule logiche, oppure, nel caso di elaborazioni in parallelo, si possono collezionare tutti i possibili risultati, e decidere se un test ha avuto successo, o meno, verificando se il risultato ottenuto rientra nel set di quelli attesi.

La bisimulation equivalence, su cui ci concentreremo, ha un approccio diverso. Ma, prima di capire cos’è la bisimulation equivalence, dobbiamo comprendere come trasformare delle specifiche formali in un labeled transition system.

In questo scenario (di processi paralleli) il non determinismo deve essere accettato. A differenza dei programmi scritti in linguaggi formali sequenziali, che è possibile trasformare in automi a stati fini deterministici, in questo caso il non determinismo non è eliminabile.

R.E. by operational semantics

Il modo più efficiente di passare dalla formalizzazione delle specifiche all’automa consiste nell’usare la operational semantics. Ma questa considera solo il passaggio da uno stato del sistema (input), ad uno stato finale (output) per una data azione a:

\[e_{initial\, state} \xrightarrow{a} f_{final\, state}\]

Questa relazione mappa ogni possibile stato iniziale per ogni possibile azione. Quindi, possiamo pensare allo stato iniziale come una configurazione del sistema. In ultima analisi i due stati (iniziale e finale) sono un labeled transition system con label a (l’azione).

Vedendolo come labeled transiton system, gli stati possono essere considerati astraendo dal loro nome, perché ci interessa osservare il comportamento. Si ricordi che stiamo osservando un sistema che interagisce con il suo ambiente, e l’interazione è veicolata dall’azione.

Quindi la operational semantics definisce una relazione binaria \((e, a, f)\) che può essere espressa tramite regole d’inferenza (inference rules) della forma:

\[\frac{premise_1, \cdots premise_n}{consequence}\]

Le regole d’inferenza definiscono la struttura del nostro sistema.

Riprendendo il ns linguaggio di specifica [7] [8]: \(\mathcal{L} ::= 0 \vert 1 \vert a \vert e_1 + e_2 \vert e_1 \cdot e_2 | e^*\) vediamo la sua operational semantics considerando come tradurre ogni termine del linguaggio in un automata che lo modella.

Avendo regular expressions, i modelli associati ai suoi termini sono finiti (? why ?). Quindi la operational semantics definisce per ogni termine automi a stati finiti non deterministici [9].

Di seguito diamo l’interpretazione di \(\mathcal{L}\). La colonna sx indica il numero di riga, la seconda colonna indica il termine in analisi, la terza colonna riporta la relativa regola d’inferenza, la colonna dx [10] indica la terminazione immediata (con successo) del sistema.

row	operator	rule	terminazione immediata
1	\(0\)	no rule
2	\(1\)	no rule	\(1 \surd\)
3	basic activity \(a\)	\(\frac{\diagup}{a \xrightarrow{a} 1}\)
4	non deterministic choice \(e_1 + e_2\)	\(\frac{e_1 \xrightarrow{a} e_1'}{(e_1 + e_2) \xrightarrow{a} e_1'}\), \(\frac{e_2 \xrightarrow{a} e_2'}{(e_1 + e_2) \xrightarrow{a} e_2'}\)	\(\frac{e_1 \surd \, or \, e_2 \surd}{(e_1 + e_2) \surd}\)
5	sequential composition \(e_1 \cdot e_2\)	\(\frac{e_1 \xrightarrow{a} e_1'}{(e_1 \cdot e_2) \xrightarrow{a} (e_1' \cdot e_2)}\) \(\frac{e_1 \surd \, , \, e_2 \xrightarrow{a} e_2'}{(e_1 \cdot e_2) \xrightarrow{a} e_2'}\)	\(\frac{e_1 \surd \, and \, e_2 \surd}{(e_1 \cdot e_2) \surd}\)
6	Kleene’s star \(e^*\)	\(\frac{e \xrightarrow{a} e'}{e^* \xrightarrow{a} (e' \cdot e^*)}\)	\(\frac{\diagup}{e^* \surd}\)

La prima riga della precedente tabella rappresenta un sistema in stato 0, ovvero in deadlock, quindi non ha terminazione immediata.

La seconda riga rappresenta un sistema in stato 1, ovvero in terminazione immediata con successo.

La terza riga analizza il sistema in grado di eseguire l’azione a. Qui non vi sono precondizioni, e la conseguenza è l’esecuzione dell’azione. Il sistema terminerà (attenzione al futuro) con successo dopo avere eseguito l’azione richiesta. Per questo motivo ora non termina con successo.

Alla riga 4 il sistema \(e_1 + e_2\) puo eseguire sia \(e_1\) che \(e_2\). Ma uno dei due deve essere deciso dal contesto. Per questo abbiamo due regole: per dare il comportamento in entrambi i casi. Ad esempio, se nell’eseguire a il sistema passa da \(e_1\) ad \(e_1'\), allora il percorso alternativo (in questo caso da \(e_2\) ad \(e_2'\)) viene eliminato.

Sempre alla riga 4, il sistema \(e_1 + e_2\) termina immediatamente, se lo stato di partenza \(e_1\) o \(e_2\) termina immediatamente. Con operatore or inclusivo, quindi se uncomponente può terminare immeditamente, lo può anche il sistema.

Alla riga 5, il sistema \(e_1 \cdot e_2\) è in grado di eseguire prima \(e_1\), e quando questo termina si passa ad eseguire \(e_2\). In generale però \(e_1\) può passare in \(e_1'\), senza terminare. In questo caso il sistema evolve in \(e_1' \cdot e_2\). Se invece \(e_1\) termina (seconda inferenza), allora parte l’elaborazione di \(e_2\), che in generale evolve nel nuovo stato \(e_2'\).

Alla riga 5, la terminazione immediata di \(e_1 \cdot e_2\) avviene solo se terminano immediatamente sia \(e_1\) che \(e_2\) (operatore and). Ad esempio \((a + 1) \cdot (b + 1)\) termina immediatamente, perché lo fanno entrambi gli 1 dei due termini che sono in non deterministic choise (operatore +). Alla stessa conclusione si arriva applicando all’esempio le regole assiomatiche.

Alla riga 6, la Kleene’s star \(e^*\) è un sistema in grado di terminare immediatamente con successo, oppure di eseguire nuovamente se stesso. In generale eseguendo l’azione a passerà dallo stato \(e\) allo stato \(e'\) per poi decidere se terminare o riprendere il ciclo, come espresso da: \(e' \cdot e^*\),

La terminazone immediata della riga 6 vale per definizione: \(e^*\) può terminare con successo immediatamente senza precondizioni.

Ad esempio \((a \, 0 \, b)^*\), per la presenza dell’operatore star può terminare immediatamente con successo, oppure eseguire l’azione a e poi andare in deadloack per la presenza dello stato 0.

A questo punto abbiamo le regole d’inferenza che ci permettono di interpretare i termini delle regular expressions. Applicandole ad un termine per volta possiamo costruire così l’automata del sistema.

Ad esempio, prendiamo \(a \cdot (b + c)\). Consideriamo:

• \(a \equiv e_1\), e
• \((b + c) \equiv e_2\).

Con la precondizione che a possa terminare immediatamente per l’azione a (espressa da \(a \xrightarrow{a} 1\)), allora la regola d’inferenza è:

\[\frac{a \xrightarrow{a} 1}{a \cdot (b + c) \xrightarrow{a} 1 \cdot (b + c)}\]

Iteriamo il ragionamento su questa regola considerando:

• \(1 \equiv e_1\), e
• \((b + c) \equiv e_2\).

Ora dovremo analizzare la non deterministic composition, che ci porta a due diverse regole d’inferenza, una ottenuta applicando l’azione b (espressa da \(b \xrightarrow{b} 1\)):

\[\frac{1 \surd , \frac{b \xrightarrow{b} 1}{(b + c) \xrightarrow{b} 1}}{1 \cdot (b + c) \xrightarrow{b} 1}\]

e l’altra applicando l’azione c (espressa da \(c \xrightarrow{c} 1\)):

\[\frac{1 \surd , \frac{c \xrightarrow{c} 1}{(b + c) \xrightarrow{c} 1}}{1 \cdot (b + c) \xrightarrow{c} 1}\]

Le regole predette portano a disegnare il seguente automa a stati finiti:

Sono stati scritti programmi che, data una formula scritta come espressione regolare, sono in grado di produrre il relativo automa a stati, usualmente nella forma:

(stato iniziale, azione, stato finale)

ovvero \((e, a, f)\).

Ricordiamo la denotational semantics associa ad un termine l’insieme delle frasi: \(e \xrightarrow{[\vert \diagup \vert]} [\![ e ]\!]\).

La operational semantics invece analizza un insieme di parole (ovvero: azioni) in sequenza, considerando l’insieme dei relativi stati ottenuti eseguendo le azioni:

\[L(e) = \{ a_1, \cdots a_n \vert e \xrightarrow{a_1} e_1 \xrightarrow{a_2} \cdots \xrightarrow{a_n} 1 \}\]

Se ci si limita all’ambito sintattico, è possibile provare che per ogni espressione regolare appartenente all’insieme di tutte le E.R., la denotational semantics equivale alle operational semantics associate con essa:

\[\text{th.} \quad \forall e \in \xi, \quad [\![ e ]\!] = L(e)\]

quindi la operational semantics è solo un modo diverso di eseguire la denotational semantics.

Ma quando si analizzano sistemi reattivi, l’aspetto è molto più complesso. Perché per ogni stato del sistema si analizzano tutte le possibili risposte che si possono ottenere in quello stato esercitanto le azioni possibili in esso. A differenza dell’analisi sintattica, che analizza una sola risposta conseguenza di una azione determinata.

---

[1]	Memo. Grammatica regolare: \[\begin{split}& A \rightarrow a\\ & A \rightarrow b C\end{split}\] dove a e b sono elementi terminali, mentre A e C sono elementi non terminali.

[2]	Grazie all’esistenza della Kleene’s star.

[3]	Per questo si parla di language (o trace) equivalence.

[4]

Per comprendere \(x \cdot 0 = 0\), si consideri la definizione di concatenazione: \(L_1 \cdot L_2 = \{uv \vert u \in L_1 \; \mathbf{and} \; v \in L_2\}\). Ma se \(L_2\) è l’insieme vuoto (si ricordi la definizione di 0), non esiste alcun \(v \in L_2\). Quindi l’operatore and è sempre false e \(x \cdot 0\) è l’insieme vuoto, ovvero 0.

[5]	Ammesso sia possibile.

[6]	Le etichette delle transizioni tra gli stati sono relative alle attività.

[7]	Attenzione al fatto che a non è un sistema che termina immediatamente; prima esegue l’azione a, poi termina con successo (1).

[8]

Ancora: questo linguaggio è il core di qualunque sistema reattivo, comprendendo gli operatori di composizione non deterministica (+), di composizione sequenziale (·) e di iterazione (la Kleene’s star). Più in generale, vi è sempre un operatore di stop con successo (1) o senza successo (0); e una serie di comandi (a). Può mancare la composizione sequenziale, sostituita ad es. da action prefixing. Oppure può mancare la Kleene’s star, sostituita da altri meccanismi di iterazione. Qui ci manca la parallel composition.

[9]	Se ci fosse anche la parallel composition, vi sarebbe la possibilità di avere un set infinito. Per ora ignoriamo questa possibilità.

[10]	Questo è un predicato, vale True se e è un sistema che può terminare immediatamente con successo.