Ritorna all'inizio

CCS

CCS (Calculus of Communicating Systems) è un'algebra di processi ideata da Robin Milner per descrivere e ragionare su sistemi concorrenti. L'idea è quella di concentrarsi su pochissimi operatori primitivi, che catturano le caratteristiche essenziali della concorrenza, fornendo una sintassi concisa per costruire e comporre processi. Non si tratta di un linguaggio di programmazione completo, ma possiede comunque piena potenza computazionale (è Turing-equivalente).

Sequenziale vs concorrente

Nei paradigmi sequenziali (si pensi a linguaggi come IMP o HOFL) valgono due proprietà comode ma limitanti:

- determinatezza: lo stesso programma, sullo stesso input, produce sempre lo stesso risultato

- due programmi che non terminano sono considerati equivalenti tra loro (entrambi denotano "bottom")

Nei paradigmi concorrenti la situazione cambia radicalmente:

- esiste un nondeterminismo intrinseco percepibile da un osservatore esterno

- la non terminazione può essere una caratteristica desiderabile (si pensi a un server, che deve restare sempre in ascolto)

- non tutti i processi non terminanti sono equivalenti tra loro

- l'interazione diventa una questione primaria

- servono dunque nuove nozioni di comportamento e di equivalenza

Per la comunicazione, CCS adotta uno scambio di messaggi binario (punto a punto) su canali. La semantica è data in stile SOS (Structural Operational Semantics) small-step, ovvero tramite un sistema di transizioni etichettate (Labelled Transition System, LTS): i processi sono gli stati, le interazioni in corso sono le etichette, e le transizioni sono definite tramite regole di inferenza per induzione sulla struttura dei processi.

Transizioni etichettate

Il cuore della semantica è la transizione etichettata

$p\stackrel{\mu }{\to }q$

dove $p$ è un processo nel suo stato corrente, $\mu$ è l'interazione in corso con l'ambiente (con gli altri processi) e $q$ è lo stato del processo dopo l'interazione. Il numero di stati e transizioni può essere infinito.

Stati ed etichette

Cosa è un processo $p$? Può essere un agente sequenziale, oppure un sistema in cui molti agenti sequenziali interagiscono.

Cosa è un'etichetta $\mu$? Può essere:

- un'azione (ad esempio un output), scritta $\alpha !v$ ("invia $v$ sul canale $\alpha$")

- una co-azione duale (ad esempio un input), scritta $\alpha ?v$ ("ricevi $v$ sul canale $\alpha$")

- un'azione interna o silenziosa $\tau$, che non comporta interazione con l'ambiente (rappresenta una comunicazione conclusa)

Possiamo essere ancora più astratti senza perdere espressività computazionale: trascuriamo i valori comunicati (come se ci fosse un canale dedicato per ciascun valore). Così:

- $\alpha !v$ diventa semplicemente $\overline{{\alpha }_v}$ oppure semplicemente $\overline{\alpha }$

- $\alpha ?v$ diventa semplicemente ${\alpha }_v$ oppure semplicemente $\alpha$

- $\lambda$ denota indifferentemente $\alpha$ oppure $\overline{\alpha }$

- $\overline{\lambda }$ denota la sua duale (assumendo $\overline{\overline{\alpha }}=\alpha$)

Le etichette di CCS

Formalmente:

- $\mathcal{C}$ è l'insieme delle azioni (input), su cui spazia $\alpha$

- $\overline{\mathcal{C}}$ è l'insieme delle co-azioni (output), su cui spazia $\overline{\alpha }$, con $\mathcal{C}\cap \overline{\mathcal{C}}=\varnothing$

- $\Lambda =\mathcal{C}\cup \overline{\mathcal{C}}$ è l'insieme delle azioni osservabili, su cui spaziano $\lambda$ e $\overline{\lambda }$

- $\tau \notin \Lambda$ è una distinta azione silenziosa

- $\mathcal{L}=\Lambda \cup \left\{\tau \right\}$ è l'insieme di tutte le azioni, su cui spazia $\mu$

Sintassi

La sintassi di CCS è definita dalla grammatica seguente (gli operatori sono elencati in ordine di precedenza):

$p,q::=\mathbf{nil}\mid x\mid \mu .p\mid p\backslash \alpha \mid p\left[\varphi \right]\mid p+q\mid p\mid q\mid \mathbf{rec}x.p$

dove:

- $\mathbf{nil}$ è il processo inattivo

- $x$ è una variabile di processo (usata per la ricorsione)

- $\mu .p$ è il prefisso d'azione

- $p\backslash \alpha$ è la restrizione di canale (canale ristretto)

- $p\left[\varphi \right]$ è la rietichettatura dei canali (channel relabelling)

- $p+q$ è la scelta nondeterministica (somma)

- $p\mid q$ è la composizione parallela

- $\mathbf{rec}x.p$ è la ricorsione

Per la precedenza, ad esempio

$\mathbf{rec}x.\mathit{coffee}.x+\mathit{tea}.\mathbf{nil}\mid \mathit{water}.\mathbf{nil}$

va letto come

$\mathbf{rec}x.\left(\left(\left(\mathit{coffee}.x\right)+\mathit{tea}.\mathbf{nil}\right)\mid \mathit{water}.\mathbf{nil}\right)$

L'unico binder è l'operatore di ricorsione $\mathbf{rec}x.p$. La nozione di variabile (di processo) libera $\mathrm{fv}\left(p\right)$ è definita come di consueto; un processo si dice chiuso se non ha variabili libere. Anche la nozione di sostituzione capture-avoiding $p\left[{}^q{/}_x\right]$ è quella usuale, e i processi sono considerati a meno di alpha-rinomina delle variabili legate, ad esempio $\mathbf{rec}x.\mathit{coin}.x=\mathbf{rec}y.\mathit{coin}.y$.

Semantica operazionale

La semantica operazionale è data dalle seguenti regole di inferenza:

- Act (prefisso d'azione)

$\frac{}{\mu .p\stackrel{\mu }{\to }p}$

- Res (restrizione)

$\frac{p\stackrel{\mu }{\to }q\mu \notin \{\alpha ,\overline{\alpha }\}}{p\backslash \alpha \stackrel{\mu }{\to }q\backslash \alpha }$

- Rel (rietichettatura)

$\frac{p\stackrel{\mu }{\to }q}{p\left[\varphi \right]\stackrel{\varphi \left(\mu \right)}{\to }q\left[\varphi \right]}$

- SumL e SumR (scelta)

$\frac{p_1\stackrel{\mu }{\to }q}{p_1+p_2\stackrel{\mu }{\to }q}\frac{p_2\stackrel{\mu }{\to }q}{p_1+p_2\stackrel{\mu }{\to }q}$

- ParL e ParR (interleaving)

$\frac{p_1\stackrel{\mu }{\to }{q}_1}{p_1\mid p_2\stackrel{\mu }{\to }{q}_1\mid p_2}\frac{p_2\stackrel{\mu }{\to }{q}_2}{p_1\mid p_2\stackrel{\mu }{\to }{p}_1\mid q_2}$

- Com (comunicazione/sincronizzazione)

$\frac{p_1\stackrel{\lambda }{\to }{q}_1{p}_2\stackrel{\overline{\lambda }}{\to }{q}_2}{p_1\mid p_2\stackrel{\tau }{\to }{q}_1\mid q_2}$

- Rec (ricorsione)

$\frac{p\left[{}^{\mathbf{rec}x.p}{/}_x\right]\stackrel{\mu }{\to }q}{\mathbf{rec}x.p\stackrel{\mu }{\to }q}$

L'LTS di CCS è di per sé infinito (uno stato per ciascun processo). L'LTS di un processo $p$ si ottiene considerando tutti gli stati raggiungibili a partire da $p$: tale LTS può essere finito oppure infinito.

Esaminiamo ora gli operatori uno per uno.

Processo Nil

$\mathbf{nil}\nrightarrow$

Il processo inattivo non fa nulla: nessuna interazione con l'ambiente è possibile. Rappresenta un agente terminato e non ha alcuna regola di semantica operazionale associata.

Prefisso d'azione

Un processo prefissato da un'azione può compiere l'azione e proseguire come previsto; l'azione può comportare un'interazione con l'ambiente. Ad esempio

$\mathit{coin}.\overline{\mathit{coffee}}.\mathbf{nil}$

attende una moneta, poi eroga un caffè e infine si ferma:

$\mathit{coin}.\overline{\mathit{coffee}}.\mathbf{nil}\stackrel{\mathit{coin}}{\to }\overline{\mathit{coffee}}.\mathbf{nil}\stackrel{\overline{\mathit{coffee}}}{\to }\mathbf{nil}$

Scelta nondeterministica

Il processo $p_1+p_2$ può comportarsi o come $p_1$ o come $p_2$. Ad esempio

$\mathit{coin}.\left(\overline{\mathit{coffee}}.\mathbf{nil}+\overline{\mathit{tea}}.\mathbf{nil}\right)$

attende una moneta, poi eroga un caffè oppure un tè, e infine si ferma.

Ricorsione

La ricorsione si comporta come una definizione ricorsiva $\mathbf{let}x=p\mathbf{in}x$. Ad esempio

$\mathbf{rec}x.\mathit{coin}.\left(\overline{\mathit{coffee}}.x+\overline{\mathit{tea}}.\mathbf{nil}\right)$

attende una moneta, poi eroga un caffè ed è di nuovo pronto, oppure eroga un tè e si ferma.

Ricorsione tramite costanti di processo

In alternativa, possiamo immaginare di avere a disposizione alcune costanti di processo $A$ insieme a un insieme $\Delta$ di dichiarazioni della forma $A\triangleq p$, una per ciascuna costante. La regola è

$\frac{A\triangleq p\in \Delta p\stackrel{\mu }{\to }q}{A\stackrel{\mu }{\to }q}$

Ad esempio $P\triangleq \mathit{coin}.\left(\overline{\mathit{coffee}}.P+\overline{\mathit{tea}}.\mathbf{nil}\right)$.

Un buffer di capacità 1 si può definire così:

$\Delta =\{B_0^1\triangleq \mathit{in}.B_1^1,B_1^1\triangleq \overline{\mathit{out}}.B_0^1\}\text{ovvero}\mathbf{rec}x.\mathit{in}.\overline{\mathit{out}}.x$

Un buffer di capacità 2:

$B_0^2\triangleq \mathit{in}.B_1^2{B}_1^2\triangleq \mathit{in}.B_2^2+\overline{\mathit{out}}.B_0^2{B}_2^2\triangleq \overline{\mathit{out}}.B_1^2$

Un buffer booleano (che ricorda l'ultimo valore inserito):

$B_{\varnothing }\triangleq {\mathit{in}}_t.B_t+{\mathit{in}}_f.B_f{B}_t\triangleq \overline{{\mathit{out}}_t}.B_{\varnothing }{B}_f\triangleq \overline{{\mathit{out}}_f}.B_{\varnothing }$

Composizione parallela

I processi in esecuzione parallela possono interlacciare (interleave) le loro azioni, oppure sincronizzarsi quando vengono compiute azioni duali (regola Com, che produce un'azione silenziosa $\tau$). Ad esempio, con

$P\triangleq \overline{\mathit{coin}}.\mathit{coffee}.\mathbf{nil}M\triangleq \mathit{coin}.\left(\overline{\mathit{coffee}}.\mathbf{nil}+\overline{\mathit{tea}}.\mathbf{nil}\right)$

abbiamo le tre possibilità:

$P\mid M\stackrel{\overline{\mathit{coin}}}{\to }\mathit{coffee}.\mathbf{nil}\mid M$

$P\mid M\stackrel{\mathit{coin}}{\to }P\mid \left(\overline{\mathit{coffee}}.\mathbf{nil}+\overline{\mathit{tea}}.\mathbf{nil}\right)$

$P\mid M\stackrel{\tau }{\to }\mathit{coffee}.\mathbf{nil}\mid \left(\overline{\mathit{coffee}}.\mathbf{nil}+\overline{\mathit{tea}}.\mathbf{nil}\right)$

È interessante mettere a confronto $B_0^1\mid B_0^1$ (due buffer di capacità 1 in parallelo) con il buffer $B_0^2$ di capacità 2: intuitivamente "simili", ma vedremo che non sono identici.

Restrizione

$\frac{p\stackrel{\mu }{\to }q\mu \notin \{\alpha ,\overline{\alpha }\}}{p\backslash \alpha \stackrel{\mu }{\to }q\backslash \alpha }$

La restrizione rende il canale $\alpha$ privato a $p$: non è possibile alcuna interazione su $\alpha$ con l'ambiente. Se $p$ è la composizione parallela di più processi, questi possono comunque sincronizzarsi su $\alpha$ (tramite la regola Com, che produce $\tau \notin \{\alpha ,\overline{\alpha }\}$ e quindi non è bloccata dalla restrizione). Ad esempio:

$\left(P\mid M\right)\backslash \mathit{coin}\backslash \mathit{coffee}\backslash \mathit{tea}\stackrel{\tau }{\to }\left(\mathit{coffee}.\mathbf{nil}\mid \overline{\mathit{coffee}}.\mathbf{nil}+\overline{\mathit{tea}}.\mathbf{nil}\right)\backslash \mathit{coin}\backslash \mathit{coffee}\backslash \mathit{tea}\stackrel{\tau }{\to }\left(\mathbf{nil}\mid \mathbf{nil}\right)\backslash \mathit{coin}\backslash \mathit{coffee}\backslash \mathit{tea}$

Abbreviazioni: dato $S=\{{\alpha }_1,\dots ,{\alpha }_n\}$ scriviamo $p\backslash S$ invece di $p\backslash {\alpha }_1\dots \backslash {\alpha }_n$; inoltre omettiamo i $\mathbf{nil}$ finali.

Rietichettatura

$\frac{p\stackrel{\mu }{\to }q}{p\left[\varphi \right]\stackrel{\varphi \left(\mu \right)}{\to }q\left[\varphi \right]}$

La rietichettatura rinomina i canali delle azioni secondo $\varphi$. Si assume $\varphi \left(\tau \right)=\tau$ e $\varphi \left(\overline{\lambda }\right)=\overline{\varphi \left(\lambda \right)}$. Permette di riusare i processi. Ad esempio, con $P\triangleq \overline{\mathit{coin}}.\mathit{coffee}$ e $\varphi \left(\mathit{coin}\right)=\mathit{moneta}$, $\varphi \left(\mathit{coffee}\right)=\mathit{caffè}$:

$P\left[\varphi \right]\stackrel{\overline{\mathit{moneta}}}{\to }\mathit{caffè}\left[\varphi \right]\stackrel{\mathit{caffè}}{\to }\mathbf{nil}\left[\varphi \right]$

La combinazione di rietichettatura, parallelo e restrizione permette di collegare buffer in cascata: dati $\eta \left(\mathit{out}\right)=c$ e $\varphi \left(\mathit{in}\right)=c$, si definisce il collegamento

$p⌢q\triangleq \left(p\left[\eta \right]\mid q\left[\varphi \right]\right)\backslash c$

così che l'uscita del primo buffer comunichi (in modo privato, sul canale $c$) con l'ingresso del secondo.

Processi guarded

La forma di ricorsione ammessa è molto generale e può produrre processi con infinite transizioni uscenti. Supponiamo $p\stackrel{\mu }{\to }q$ e prendiamo $P\triangleq \mathbf{rec}x.p\mid x$ (ovvero $P\triangleq p\mid P$): allora

$P\stackrel{\mu }{\to }q\mid PP\stackrel{\mu }{\to }p\mid q\mid PP\stackrel{\mu }{\to }p\mid p\mid q\mid P\dots$

Tali processi sono detti infinitely branching e sono indesiderabili (BAD).

I processi guarded garantiscono che le variabili di processo compaiano sotto un prefisso (la ricorsione è "protetta" da qualche azione). Sia $X$ un insieme di variabili di processo. Il predicato $G\left(p,X\right)$ ("tutti i nomi definiti ricorsivamente sono guarded in $p$, cioè se un nome di $X$ occorre libero in $p$ allora è prefissato da un'azione") è definito per induzione:

$G\left(\mathbf{nil},X\right)\triangleq \mathbf{true}G\left(p\left[\varphi \right],X\right)\triangleq G\left(p,X\right)$

$G\left(x,X\right)\triangleq x\notin XG\left(p+q,X\right)\triangleq G\left(p,X\right)\wedge G\left(q,X\right)$

$G\left(\mu .p,X\right)\triangleq G\left(p,\varnothing \right)G\left(p\mid q,X\right)\triangleq G\left(p,X\right)\wedge G\left(q,X\right)$

$G\left(p\backslash \alpha ,X\right)\triangleq G\left(p,X\right)G\left(\mathbf{rec}x.p,X\right)\triangleq G\left(p,X\cup \left\{x\right\}\right)$

Un processo chiuso $p$ è guarded se $G\left(p,\varnothing \right)$ è vero. Si noti la clausola chiave $G\left(\mu .p,X\right)\triangleq G\left(p,\varnothing \right)$: passare sotto un prefisso "azzera" l'insieme dei nomi da proteggere, poiché essi risultano ormai guardati dall'azione $\mu$.

Esempi:

- $\mathbf{rec}x.x$ — unguarded

- $\mathbf{rec}x.\alpha .\mathbf{rec}y.x$ — guarded

- $\mathbf{rec}x.\alpha .\mathbf{rec}y.x+y$ — unguarded (la $y$ non è guardata)

- $\mathbf{rec}x.\alpha .\mathbf{rec}y.x\mid y$ — unguarded

- $\mathbf{rec}x.\alpha .\mathbf{rec}y.x\mid \beta .y$ — guarded

Valgono inoltre alcune proprietà (dimostrabili per induzione strutturale):

- $G\left(p,X\cup \left\{x\right\}\right)\Rightarrow G\left(p,X\right)$

- $G\left(p,X\right)\wedge x\notin \mathrm{fv}\left(p\right)\Rightarrow G\left(p,X\cup \left\{x\right\}\right)$

- le sostituzioni preservano la guardedness: $G\left(p,X\right)\wedge {\bigwedge }_{i\in \left[1,n\right]}G\left(p_i,X\right)\Rightarrow G\left(p\left[{}^{p_1}{/}_{x_1},\dots {,}^{p_n}{/}_{x_n}\right],X\right)$

- le transizioni preservano la guardedness: $G\left(p,X\right)\wedge p\stackrel{\mu }{\to }q\Rightarrow G\left(q,\varnothing \right)$

Il risultato fondamentale è che i processi guarded sono finitely branching:

$G\left(p,\varnothing \right)\Rightarrow \forall \mu .\{q\mid p\stackrel{\mu }{\to }q\}\text{è un insieme finito}$

CCS con passaggio di valori

Anche reintroducendo i valori, possiamo ricondurci al caso astratto. Le regole sono

$\frac{}{\alpha !v.p\stackrel{\overline{{\alpha }_v}}{\to }p}\frac{}{\alpha ?x.p\stackrel{{\alpha }_v}{\to }p\left[{}^v{/}_x\right]}$

Quando l'insieme dei valori è finito, $V\triangleq \{v_1,\dots ,v_n\}$, si ha

$\alpha !v.p\equiv \overline{{\alpha }_v}.p\alpha ?x.p\equiv {\alpha }_{v_1}.p\left[{}^{v_1}{/}_x\right]+\cdots +{\alpha }_{v_n}.p\left[{}^{v_n}{/}_x\right]$

e un costrutto di tipo `receive ... end` con casi $v\to p$, $w\to q$ e default $\backslash \_$$\to r$ corrisponde a ${\alpha }_v.p+{\alpha }_w.q+{\sum }_{z\ne v,w}{\alpha }_z.r$.

Semantica astratta

Processi sintatticamente diversi possono esibire esattamente lo stesso comportamento. Vogliamo dunque una nozione di equivalenza che astragga dalla particolare sintassi. Ne esaminiamo tre, di "forza" decrescente.

Isomorfismo di grafi

Dati due LTS $G=\left(V,E\right)$ e $G^{\prime }=\left(V^{\prime },E^{\prime }\right)$, una biiezione $f:V\to V^{\prime }$ è un isomorfismo se preserva e riflette le transizioni etichettate:

$v\stackrel{\mu }{\to }w\iff f\left(v\right)\stackrel{\mu }{\to }f\left(w\right)$

L'isomorfismo astrae dai nomi degli stati. Cattura ad esempio le equivalenze

$\mathbf{nil}\cong \mathbf{nil}\backslash \alpha \cong \mathbf{nil}\left[\varphi \right]p\cong p+\mathbf{nil}\cong p+p\cong p\mid \mathbf{nil}p+q\cong q+pp\mid q\cong q\mid p$

Tuttavia l'isomorfismo è troppo stretto: $B_0^2$ e $B_0^1\mid B_0^1$ sono intuitivamente equivalenti (entrambi buffer di capacità 2) ma i loro LTS non sono isomorfi (il primo ha 3 stati, il secondo 4). Analogamente $\mathbf{rec}x.\alpha .x$, $\mathbf{rec}x.\alpha .\alpha .x$ e $\alpha .\mathbf{rec}x.\alpha .x$ sono intuitivamente equivalenti ma non isomorfi.

Equivalenza di tracce

In teoria degli automi corrisponde all'equivalenza di linguaggi. Una traccia (finita) è una sequenza di etichette etichettante un cammino

$p\stackrel{{\mu }_1{\mu }_2\cdots {\mu }_k}{\to }q\text{ovvero}p=p_0\stackrel{{\mu }_1}{\to }{p}_1\stackrel{{\mu }_2}{\to }\cdots \stackrel{{\mu }_k}{\to }{p}_k=q$

La semantica di tracce di un processo è

$\mathcal{T}\left(p\right)=\{{\mu }_1{\mu }_2\cdots {\mu }_k\mid \exists q.p\stackrel{{\mu }_1{\mu }_2\cdots {\mu }_k}{\to }q\}$

Due processi sono trace equivalent se hanno la stessa semantica di tracce: $p{\equiv }_{\mathrm{tr}}q$ se e solo se $\mathcal{T}\left(p\right)=\mathcal{T}\left(q\right)$. L'isomorfismo implica l'equivalenza di tracce, e la semantica di tracce è prefix-closed (se una traccia è presente, lo sono tutti i suoi prefissi).

L'equivalenza di tracce risolve i casi visti sopra (ad esempio $\mathcal{T}\left(B_0^2\right)=\mathcal{T}\left(B_0^1\mid B_0^1\right)$, descrivibile dal vincolo $0\le \#\mathit{in}-\#\mathit{out}\le 2$ su ogni prefisso). Tuttavia è troppo grossolana: identifica processi che intuitivamente vorremmo distinguere. Confrontiamo le due distributrici

$\mathit{coin}.\left(\overline{\mathit{coffee}}+\overline{\mathit{tea}}\right)\text{e}\mathit{coin}.\overline{\mathit{coffee}}+\mathit{coin}.\overline{\mathit{tea}}$

Sono trace equivalenti, ma profondamente diverse dal punto di vista del cliente: nella prima inserisco la moneta e poi scelgo io la bevanda; nella seconda inserisco la moneta e la macchina sceglie per me. La differenza diventa drammatica componendo le macchine con un cliente $C\triangleq \overline{\mathit{coin}}.\mathit{coffee}.C$ che vuole solo caffè: con la seconda macchina si può raggiungere un deadlock.

Verso la bisimilarità

Riassumendo:

- l'isomorfismo di grafi distingue troppi processi

- l'equivalenza di tracce identifica troppi processi

- serve una nozione di equivalenza intermedia: la bisimilarità (forte)

L'idea guida è: due processi sono equivalenti a meno che non si abbia una buona ragione per distinguerli.

Il gioco della bisimulazione

La bisimulazione può essere descritta come un gioco tra due processi $p,q$ e due giocatori avversari:

- Alice, l'attaccante, vuole dimostrare che $p$ e $q$ non sono equivalenti

- Bob, il difensore, vuole dimostrare che $p$ e $q$ sono equivalenti

Il gioco è a turni; a ogni turno:

- Alice sceglie uno dei due processi e una sua transizione uscente

- Bob deve rispondere con una transizione dell'altro processo, con la stessa etichetta scelta da Alice

- al turno successivo, se c'è, si considera l'equivalenza dei processi di arrivo

Alice vince se a un certo punto riesce a fare una mossa che Bob non può eguagliare. Bob vince in tutti gli altri casi (se Alice non trova mosse, o se il gioco non termina). Alice ha una strategia vincente se riesce a confutare l'equivalenza di $p$ e $q$ in un numero finito di mosse.

Nell'esempio delle due distributrici, Alice gioca $\mathit{coin}.\overline{\mathit{coffee}}+\mathit{coin}.\overline{\mathit{tea}}\stackrel{\mathit{coin}}{\to }\overline{\mathit{coffee}}$; Bob può solo rispondere $\mathit{coin}.\left(\overline{\mathit{coffee}}+\overline{\mathit{tea}}\right)\stackrel{\mathit{coin}}{\to }\overline{\mathit{coffee}}+\overline{\mathit{tea}}$; poi Alice gioca $\overline{\mathit{coffee}}+\overline{\mathit{tea}}\stackrel{\overline{\mathit{tea}}}{\to }\mathbf{nil}$ e Bob non può replicare (da $\overline{\mathit{coffee}}$ non c'è una $\overline{\mathit{tea}}$): Alice vince.

Bisimulazione forte

La nozione di bisimulazione non è ristretta a CCS: si applica a qualsiasi LTS. Sia $\mathcal{P}$ l'insieme dei processi e $\mathbf{R}\subseteq \mathcal{P}\times \mathcal{P}$ una relazione binaria (scriviamo $p\mathbf{R}q$ quando $\left(p,q\right)\in \mathbf{R}$). $\mathbf{R}$ è una bisimulazione forte se

$\forall p,q.\left(p,q\right)\in \mathbf{R}\Rightarrow \{\begin{array}{l}\forall \mu ,p^{\prime }.p\stackrel{\mu }{\to }{p}^{\prime }\Rightarrow \exists q^{\prime }.q\stackrel{\mu }{\to }{q}^{\prime }\wedge p^{\prime }\mathbf{R}{q}^{\prime }\\ \wedge \\ \forall \mu ,q^{\prime }.q\stackrel{\mu }{\to }{q}^{\prime }\Rightarrow \exists p^{\prime }.p\stackrel{\mu }{\to }{p}^{\prime }\wedge p^{\prime }\mathbf{R}{q}^{\prime }\end{array}$

Intuitivamente: se due processi sono in relazione, allora per ogni mossa di Alice, Bob può trovare una mossa che porta a processi ancora in relazione (cioè Bob ha una strategia vincente). Con "forte" si intende che tutte le transizioni, comprese quelle silenziose $\tau$, devono essere eguagliate.

Esempi di bisimulazioni forti:

- $\varnothing$ è una bisimulazione forte

- l'identità $\mathit{Id}\triangleq \{\left(p,p\right)\mid p\in \mathcal{P}\}$ è una bisimulazione forte

- ogni isomorfismo di grafi definisce una bisimulazione forte ${\mathbf{R}}_f\triangleq \left\{\left(p,f\left(p\right)\right)\right\}$

A differenza degli isomorfismi, però, in una bisimulazione lo stesso processo può essere in relazione con molti processi. Ad esempio:

$\mathbf{R}\triangleq \{\left(\mathbf{rec}x.\alpha .x,\mathbf{rec}x.\alpha .\alpha .x\right),\left(\mathbf{rec}x.\alpha .x,\alpha .\mathbf{rec}x.\alpha .\alpha .x\right)\}$

e, per i buffer,

$\mathbf{R}\triangleq \{\left(B_0^2,B_0^1\mid B_0^1\right),\left(B_1^2,B_1^1\mid B_0^1\right),\left(B_1^2,B_0^1\mid B_1^1\right),\left(B_2^2,B_1^1\mid B_1^1\right)\}$

Proprietà di chiusura

Le bisimulazioni forti godono di buone proprietà di chiusura (le dimostrazioni sono tutte molto simili: si "segue" la mossa nella bisimulazione disponibile):

- Unione: se ${\mathbf{R}}_1$ e ${\mathbf{R}}_2$ sono bisimulazioni forti, allora ${\mathbf{R}}_1\cup {\mathbf{R}}_2$ lo è

- Inversa: se $\mathbf{R}$ è una bisimulazione forte, allora ${\mathbf{R}}^{-1}\triangleq \{\left(q,p\right)\mid p\mathbf{R}q\}$ lo è

- Composizione: se ${\mathbf{R}}_1$ e ${\mathbf{R}}_2$ sono bisimulazioni forti, allora ${\mathbf{R}}_2\circ {\mathbf{R}}_1\triangleq \{\left(p,q\right)\mid \exists r.p{\mathbf{R}}_{1}r\wedge r{\mathbf{R}}_{2}q\}$ lo è (la composizione si scrive talvolta anche ${\mathbf{R}}_1{\mathbf{R}}_2$)

Bisimilarità forte

La bisimilarità forte $\simeq$ (spesso denotata $\sim$ in letteratura; usiamo $\simeq$ per ricordare che è una congruenza) è la più grande bisimulazione forte:

$p\simeq q\text{sse}\exists \mathbf{R}\text{bisimulazione forte con}\left(p,q\right)\in \mathbf{R}\text{ovvero}\simeq \triangleq {\bigcup }_{\mathbf{R}\text{s.b.}}\mathbf{R}$

Per dimostrare che due processi sono fortemente bisimili è dunque sufficiente esibire una bisimulazione forte che li contiene. Questa è la stessa relazione che la nota [[bisimulazione]] caratterizza come punto fisso del funzionale $\Phi$ tramite il Teorema di Kleene.

Una singola bisimulazione forte non è necessariamente una relazione di equivalenza, ma la bisimilarità sì.

Teorema. La bisimilarità forte è una relazione di equivalenza ($\mathit{Id}\subseteq \simeq$ per la riflessività; la simmetria segue dalla chiusura per inversa; la transitività dalla chiusura per composizione).

Teorema. La bisimilarità forte è essa stessa una bisimulazione forte (segue dalla chiusura per unione). Di conseguenza essa è la più grande bisimulazione forte, e ogni altra bisimulazione forte è contenuta in $\simeq$.

Teorema (definizione ricorsiva). $\simeq$ soddisfa

$\forall p,q.p\simeq q\iff \{\begin{array}{l}\forall \mu ,p^{\prime }.p\stackrel{\mu }{\to }{p}^{\prime }\Rightarrow \exists q^{\prime }.q\stackrel{\mu }{\to }{q}^{\prime }\wedge p^{\prime }\simeq q^{\prime }\\ \wedge \\ \forall \mu ,q^{\prime }.q\stackrel{\mu }{\to }{q}^{\prime }\Rightarrow \exists p^{\prime }.p\stackrel{\mu }{\to }{p}^{\prime }\wedge p^{\prime }\simeq q^{\prime }\end{array}$

(la direzione $\Rightarrow$ è immediata perché $\simeq$ è una bisimulazione forte; la direzione $\Leftarrow$ si dimostra mostrando che $\mathbf{R}\triangleq \left\{\left(p,q\right)\right\}\cup \simeq$ è una bisimulazione forte).

Relazione ed equivalenza indotta

Ogni relazione $\mathbf{R}$ induce un'equivalenza ${\equiv }_{\mathbf{R}}$, la più piccola equivalenza che contiene $\mathbf{R}$ (chiusura riflessiva, simmetrica e transitiva). Se $\mathbf{R}$ è una bisimulazione forte, allora anche ${\equiv }_{\mathbf{R}}$ lo è. Ogni equivalenza induce a sua volta una partizione in classi di equivalenza ${\left[p\right]}_{\equiv }=\{q\mid p\equiv q\}$; nella pratica, invece di elencare tutte le coppie di ${\equiv }_{\mathbf{R}}$, conviene elencarne soltanto le classi.

Compositionalità

Un'equivalenza $\equiv$ è una congruenza quando è preservata da ogni contesto:

$\forall ℂ[\cdot ].\forall p,q.p\equiv q\Rightarrow ℂ\left[p\right]\equiv ℂ\left[q\right]$

In tal caso possiamo sostituire processi equivalenti in qualsiasi contesto senza alterare la semantica astratta — proprietà essenziale per il ragionamento composizionale.

Teorema. La bisimilarità forte è una congruenza. In particolare, per ogni operatore:

1. $p\simeq q\Rightarrow \mu .p\simeq \mu .q$

2. $p\simeq q\Rightarrow p\backslash \alpha \simeq q\backslash \alpha$

3. $p\simeq q\Rightarrow p\left[\varphi \right]\simeq q\left[\varphi \right]$

4. $p_0\simeq q_0\wedge p_1\simeq q_1\Rightarrow p_0+p_1\simeq q_0+q_1$

5. $p_0\simeq q_0\wedge p_1\simeq q_1\Rightarrow p_0\mid p_1\simeq q_0\mid q_1$

La tecnica di dimostrazione è sempre la stessa: si "indovina" una relazione abbastanza grande da contenere tutte le coppie di interesse, si mostra che è una bisimulazione forte, e dunque essa è contenuta in $\simeq$. Per i casi della scelta (4) e del parallelo si deve aggiungere $\cup \simeq$ alla relazione candidata, poiché i processi di arrivo possono essere già bisimili senza essere strutturalmente della forma prevista.

CCS: alcune leggi

Tutte le leggi seguenti valgono a meno di bisimilarità forte e si dimostrano esibendo una bisimulazione forte opportuna.

Per scelta e parallelo (monoidi commutativi, con $+$ anche idempotente):

$p+\mathbf{nil}\simeq pp\mid \mathbf{nil}\simeq p$

$p+q\simeq q+pp\mid q\simeq q\mid p$

$p+\left(q+r\right)\simeq \left(p+q\right)+rp\mid \left(q\mid r\right)\simeq \left(p\mid q\right)\mid r$

$p+p\simeq p$

Per la restrizione:

$\mathbf{nil}\backslash \alpha \simeq \mathbf{nil}$

$\left(\mu .p\right)\backslash \alpha \simeq \mathbf{nil}\text{se}\mu \in \{\alpha ,\overline{\alpha }\}$

$\left(\mu .p\right)\backslash \alpha \simeq \mu .\left(p\backslash \alpha \right)\text{se}\mu \notin \{\alpha ,\overline{\alpha }\}$

$\left(p+q\right)\backslash \alpha \simeq \left(p\backslash \alpha \right)+\left(q\backslash \alpha \right)$

$p\backslash \alpha \backslash \alpha \simeq p\backslash \alpha p\backslash \alpha \backslash \beta \simeq p\backslash \beta \backslash \alpha$

Per la rietichettatura:

$\mathbf{nil}\left[\varphi \right]\simeq \mathbf{nil}$

$\left(\mu .p\right)\left[\varphi \right]\simeq \varphi \left(\mu \right).\left(p\left[\varphi \right]\right)$

$\left(p+q\right)\left[\varphi \right]\simeq \left(p\left[\varphi \right]\right)+\left(q\left[\varphi \right]\right)$

$p\left[\varphi \right]\left[\eta \right]\simeq p\left[\eta \circ \varphi \right]$

Articoli correlati