diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 5315cd8..8690022 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -213,6 +213,7 @@ }, "active": "56150e6df7869900", "lastOpenFiles": [ + "Pasted image 20250428083727.png", "Concurrent Systems/slides/class 13.pdf", "Concurrent Systems/notes/13 - Weak Bisimilarity.md", "Concurrent Systems/notes/12 - Calculus of communicating system.md", diff --git a/Concurrent Systems/notes/13 - Weak Bisimilarity.md b/Concurrent Systems/notes/13 - Weak Bisimilarity.md index 2f7406f..6a9bac0 100644 --- a/Concurrent Systems/notes/13 - Weak Bisimilarity.md +++ b/Concurrent Systems/notes/13 - Weak Bisimilarity.md @@ -24,4 +24,18 @@ $\approx$ is a 1. equivalence 2. congruence 3. weak bisimulation -4. $\sim a$ \ No newline at end of file +4. $\sim \subset \approx$ + +#### Examples of weakly bisimilar processes +![](../../Pasted%20image%2020250428083727.png) + +**Theorem:** given any process P and any sum M, N, then: +1. $P \approx \tau.{P}$ +2. $M+N+\tau.N \approx M + \tau.N$ +3. $M+\alpha.P+\alpha.(N+\tau.P) \approx M + \alpha.(N + \tau.P)$ + +*Proof:* +take the symmetric closure of the following relations, that can be easily shown to be weak simulations: +1. $S = \{ P,\tau.P \}\cup Id$ +2. $S=\{ M+N+\tau.N,M+\tau.N \}\cup Id$ +3. $S=\\{ (M+\alpha.P+) \}$ \ No newline at end of file diff --git a/Pasted image 20250428083727.png b/Pasted image 20250428083727.png new file mode 100644 index 0000000..b0c7d9c Binary files /dev/null and b/Pasted image 20250428083727.png differ