vault backup: 2025-04-28 18:01:27

Concurrent Systems/notes/13 - Weak Bisimilarity.md

@@ -103,3 +103,9 @@ The specification is: $$L \triangleq \tau.\bar{p_{1}}L+\tau.\bar{p_{2}}.L+\dots+
 where $\tau$'s represent ball extractions and $\tilde{p_{i}}$ is the action that communicates with the value of the extracted ball. The LTS resulting from this specification is:
 ![](../../Pasted%20image%2020250428175449.png)
 
+We now build a system with n components, one for every ball.
+
+Every component can be in three states:
+- A (waiting for being habilitated to extraction)
+- B (habilitated, with the possibility of being extracted or of habilitating the next component)
+- 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}$$