diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 2ecb80d..d8d6c46 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -193,6 +193,7 @@ }, "active": "ec8d1a91f1f0cc7e", "lastOpenFiles": [ + "Pasted image 20250430175412.png", "Pasted image 20250430171336.png", "Concurrent Systems/slides/class 13.pdf", "Concurrent Systems/notes/13 - Weak Bisimilarity.md", @@ -209,7 +210,6 @@ "Concurrent Systems/notes/images/Pasted image 20250429085319.png", "Concurrent Systems/notes/images/Pasted image 20250429084950.png", "Concurrent Systems/notes/images/Pasted image 20250429084921.png", - "Concurrent Systems/notes/images/Pasted image 20250429084358.png", "Concurrent Systems/slides/class 12.pdf", "Concurrent Systems/notes/11 - LTSs and Bisimulation.md", "HCIW/slides/HCI in the car.pdf", diff --git a/Concurrent Systems/notes/13 - Weak Bisimilarity.md b/Concurrent Systems/notes/13 - Weak Bisimilarity.md index 9bc9f22..3a8e6d8 100644 --- a/Concurrent Systems/notes/13 - Weak Bisimilarity.md +++ b/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}$$ diff --git a/Pasted image 20250430175412.png b/Pasted image 20250430175412.png new file mode 100644 index 0000000..582c7a9 Binary files /dev/null and b/Pasted image 20250430175412.png differ