vault backup: 2025-04-30 17:18:22

Concurrent Systems/notes/13 - Weak Bisimilarity.md

@@ -111,7 +111,9 @@ Every component can be in three states:
 - C (extracted, waiting to externally communicate its value and start the process again): $$A_{i}=a_{i}.B_{i} \quad B_{i}=\tau.C_{i}+\bar{a}_{(i \space mod \space n)+1}.A_{i} \quad C_{i}=\bar{p}_{i}.B_{i}$$
 In pratica ogni volta o estrae di nuovo "se stesso" oppure "abilita" il componente successivo.
 
-Implementation: $$Impl \triangleq (B_{1}|A_{2}|\dots|An)$$
+Implementation: $$Impl \triangleq (B_{1}|A_{2}|\dots|An)\setminus_{\{ a_{1}\dots an \}}$$
 basically we need to have an initially habilitated process, which can be any (the first one in our case).
 
-This will generate the LTS:
+This will generate the LTS:
+![500](../../Pasted%20image%2020250430171336.png)
+