diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index d8b6a8a..69c3e6f 100644 --- a/.obsidian/workspace.json +++ b/.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" ] diff --git a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md index 613e6a5..6bc6280 100644 --- a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md +++ b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md @@ -48,4 +48,9 @@ A binary relation S ⊆ Q×Q is a simulation if and only if We say that p is simulated by q if there exists a simulation S such that $$(p,q) ∈ S$$ 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. \ No newline at end of file +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) \ No newline at end of file diff --git a/Pasted image 20250408094749.png b/Pasted image 20250408094749.png new file mode 100644 index 0000000..569d0c1 Binary files /dev/null and b/Pasted image 20250408094749.png differ