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

Concurrent Systems/notes/13 - Weak Bisimilarity.md

@@ -139,3 +139,9 @@ The specification is:
 if $i \in X$ then:
 $$S_{i,X}=\sum_{j \in X}b_{j}.S_{i,X-\{ j \}}$$
 otherwise: $$S_{i,X}=a_{i}.S_{(i \space mod \space n)+1,X\cup \{ i \}} + \sum_{j \in X}b_{j}.S_{i,X-\{ j \}}$$
+Starting config $S_{1,\{  \}}$
+LTS for $n=2$:
+![](../../Pasted%20image%2020250430175412.png)
+
+We can try to implement the scheduler in the following way:
+$$A_{i}=a_{i}.B_{i} \quad B_{i}=\bar{c}_{(i \space mod \space n)+1}.C_{i} \quad C_{i}=b_{i}.D_{i} \quad D_{i}=c_{i}.A_{i}$$