LEGGI STATICHE

Leggi della Composizione parallela:

1. $P\:\vert\:Q \:=\: Q\:\vert\:P \qquad$ (commutatività)
2. $P\:\vert\:(Q\:\vert\:R) \:=\: (P\:\vert\:Q)\:\vert\:R \qquad$ (associatività)
3. $P\:\vert\:nil \:=\: P \qquad$ ($nil$ è l'elemento identità anche per la composizione)

Leggi della Relabelling:

1. $P\:\backslash L \:=\: P \qquad$ (se $P$ non ha azioni in $L \cup \overline{L}$)
2. $P\:\backslash K\:\backslash L \:=\: P \:\backslash (K\cup L)$
3. $P[f]\:\backslash L \:=\: P\:\backslash f^{-1}(L)[f]$
4. $(P\:\vert\:Q)\:\backslash L \:=\: P\:\backslash L\:\vert\:Q\:\backslash L \qquad$ (se $P$ e $Q$ non sincronizzano su azioni di $L$)

La legge $(1)$ assicura che le azioni $\alpha \in L$ non appariranno visibili nel sistema, l'operatore di restizione diventa così superfluo. La Legge $(2)$ è una ovvia conseguenza logica; a legge $(3)$ asserisce che l'operatore di restrizione e di relabelling commutano mediante piccoli aggiustamenti, la legge $(4)$ infine, è un tipo di legge distributiva che ci permette di distribuire l'operazione di restrizione sull'operazione di composizione parallela sino a quando le azioni interessate alla restizione non sono possibili veicoli di comunicazione.

Leggi del Relabelling (con Id funzione identità):

1. $P[Id] \:=\: P$
2. $P[f]\:=\:P[f'] \qquad$ (se $f$ e $f'$ sono uguali sull'insieme di azioni di $P$)
3. $P[f][f'] \:=\: P[f'\circ f]$
4. $(P\:\vert\:Q)[f] \:=\: P[f]\:\vert\:Q[f] \qquad$ (se $f$ ristretta alle azioni di $P \:\vert\: Q$ è iniettiva)

La legge $(1)$ è la funzione identità, la legge $(2)$ assicura che $f$ e $f'$ sortiranno lo stesso effetto su $P$, la legge $(3)$ sfrutta la definizione di composizione di funzioni e a legge $(4)$ assicura che non verranno creati più canali di comunicazione di quelli esistenti prima di distribuire l'operatore di relabelling (garantito dall'iniettività).

Alcuni esempi che si possono ottenere combinando le leggi statiche

Esempio 3..1  

1. $P[b/a] \:=\: P \: se \:a,\overline a \notin \:\mathcal{L}(P)$
2. $P\backslash a\:=\:P[b/a]\backslash b \:=\: P \:se \:b,\overline b \notin \:\mathcal{L}(P)$
3. $P\backslash [b/c]\:=\:P[b/c]\backslash a \: se \:b,c \neq \: a$

Nel esempio $2(1)$ si utilizzano le leggi $(2)$ e $(1)$ delle leggi di relabelling; nell'esempio $2(2)$ si utilizzano le proposizioni $(2)$ e $(1)$ delle leggi di restizione e la proposizione $(1)$ delle leggi di relabelling; nell'esempio $2(3)$ si utilizzza la proposizione $(2)$ e $(1)$ delle leggi di relabelling.