diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 3c089ed..eac2cd9 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -242,6 +242,7 @@ "lastOpenFiles": [ "Concurrent Systems/slides/class 11.pdf", "Concurrent Systems/notes/11 - LTSs and Bisimulation.md", + "Pasted image 20250414084615.png", "Pasted image 20250414082824.png", "Concurrent Systems/notes/12.md", "Concurrent Systems/slides/class 12.pdf", @@ -284,7 +285,6 @@ "Foundation of data science/class 9.pdf", "Concurrent Systems/slides/class 10.pdf", "Concurrent Systems/ignore this folder", - "Concurrent Systems/notes/images/Pasted image 20250401083747.png", "Senza nome.canvas" ] } \ No newline at end of file diff --git a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md index 24c624b..233a80e 100644 --- a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md +++ b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md @@ -60,4 +60,10 @@ If S contained one among (p1,q1) or (p1,q2), then it would not be a simulation: p0 is simulated by q0: $$S = {(p0, q0), (p1, q2), (p2, q3)}$$ q0 is simulated by p0: $$S′ ={(q0,p0),(q1,p1),(q2,p1),(q3,p2)}$$ -However, p0 and q0 are not bisimilar: the transition q0 -> a -> q1 is not bisimulable by any transition from p0 (ndeed, p0 –a–> p1 does not suffice, because p1 can perform a b and so cannot be bisimilar to q1). \ No newline at end of file +However, p0 and q0 are not bisimilar: the transition q0 -> a -> q1 is not bisimulable by any transition from p0 (ndeed, p0 –a–> p1 does not suffice, because p1 can perform a b and so cannot be bisimilar to q1). + +#### Bisimulation is NOT isomorfism +![](../../Pasted%20image%2020250414084615.png) + +$S = \{(p0,q0), (p1,q1), (p2,q1), (p0,q2)\}$ +$S^{−1} = \{(q0,p0), (q1,p1), (q1,p2), (q2,p0)\}$ diff --git a/Pasted image 20250414084615.png b/Pasted image 20250414084615.png new file mode 100644 index 0000000..622a774 Binary files /dev/null and b/Pasted image 20250414084615.png differ