vault backup: 2025-04-14 18:15:00

Concurrent Systems/notes/12 - CCS (che non so cosa voglia dire).md

@@ -177,4 +177,11 @@ $$\frac{a.A' \xrightarrow{a} A' \quad A \triangleq a.A'}{A \xrightarrow{a} A'}
 since $b$ is in $\{b, \bar{b}\}$, we will NOT see the transitions:
 $$\frac{\frac{\frac{b.B' \xrightarrow{b} B' \quad B \triangleq b.B'}{B \xrightarrow{b} B'}}
 {{A \mid B \xrightarrow{b} A \mid B'}}b \in \{b, \bar{b}\}}{{(A \mid B) \setminus b}}$$
-This time I won't split it in separate pieces since I don't feel like doing it, just buy glasses.
+This time I won't split it in separate pieces since I don't feel like doing it, just buy glasses.
+
+###### So... What if we restrict on b?
+- The effect of the restriction on b is that we have deleted the transitions involving b (hide all transitions labelled with $b$ and $\bar{b}$).
+- Notice that the τ, even if it has been generated by synchronizing on b, it is still present after applying the restriction on b!
+	- the purpose of the τ is exactly to signal that a synchronization has happened but to hide the event on which the involved processed synchronized.
+
+- In general, it is possible that whole states disappear upon restriction of some names: this would be the case, e.g., if we consider the LTS arising from $(A’ | B)\setminus a,b$:![](../../Pasted%20image%2020250414181443.png)