vault backup: 2025-04-08 09:51:02

.obsidian/workspace.json

@@ -213,6 +213,7 @@
   "lastOpenFiles": [
     "Concurrent Systems/slides/class 11.pdf",
     "Concurrent Systems/notes/11 - LTSs and Bisimulation.md",
+    "Pasted image 20250408094749.png",
     "Pasted image 20250408093840.png",
     "Pasted image 20250408092853.png",
     "Pasted image 20250408091924.png",
@@ -254,7 +255,6 @@
     "Concurrent Systems/notes/images/Pasted image 20250401083747.png",
     "Concurrent Systems/notes/images/Pasted image 20250401092557.png",
     "Concurrent Systems/slides/class 6.pdf",
-    "Concurrent Systems/notes/images/Pasted image 20250325090735.png",
     "Concurrent Systems/slides/class 8.pdf",
     "Senza nome.canvas"
   ]

Concurrent Systems/notes/11 - LTSs and Bisimulation.md

@@ -49,3 +49,8 @@ We say that p is simulated by q if there exists a simulation S such that $$(p,q)
 We say that S is a bisimulation if both S and S−1 are simulations (where $$S^{-1} = \{(p,q) : (q,p) ∈ S\}$$)
 
 Two states q and p are bisimulation equivalent (or, simply, bisimilar) if there exists a bisimulation S such that (p, q) ∈ S; we shall then write p ∼ q.
+
+![](../../Pasted%20image%2020250408094749.png)
+q0 is simulated by p0; this is shown by the following simulation relation: $$S = \{(q0,p0), (q1,p1), (q2,p1), (q3,p2), (q4,p3)\}$$
+To let p0 be simulated by q0, we should have that p1 is simulated by q1 or q2.
+If S contained one among (p1,q1) or (p1,q2), then it would not be a simulation: indeed, p1 can perform both a c (whereas q1 cannot) and a b (whereas q2 cannot)