diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 8ea6b05..3c089ed 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -4,22 +4,71 @@ "type": "split", "children": [ { - "id": "67c0c397411f4359", + "id": "ceb8ca67f2b32f40", "type": "tabs", + "dimension": 44.34097421203438, "children": [ { - "id": "9247ae5d7ced22e9", + "id": "fbeaa35cc5a8abf1", + "type": "leaf", + "state": { + "type": "markdown", + "state": { + "file": "Concurrent Systems/notes/11 - LTSs and Bisimulation.md", + "mode": "source", + "source": false + }, + "icon": "lucide-file", + "title": "11 - LTSs and Bisimulation" + } + }, + { + "id": "84845736e00d5c98", + "type": "leaf", + "state": { + "type": "markdown", + "state": { + "file": "Concurrent Systems/notes/12.md", + "mode": "source", + "source": false + }, + "icon": "lucide-file", + "title": "12" + } + } + ] + }, + { + "id": "dd628773839aa478", + "type": "tabs", + "dimension": 55.65902578796562, + "children": [ + { + "id": "2882ba3b76891dd0", "type": "leaf", "state": { "type": "pdf", "state": { - "file": "HCIW/slides/Zooming interfaces.pdf" + "file": "Concurrent Systems/slides/class 12.pdf" }, "icon": "lucide-file-text", - "title": "Zooming interfaces" + "title": "class 12" + } + }, + { + "id": "364a7591f14f033a", + "type": "leaf", + "state": { + "type": "pdf", + "state": { + "file": "Concurrent Systems/slides/class 11.pdf" + }, + "icon": "lucide-file-text", + "title": "class 11" } } - ] + ], + "currentTab": 1 } ], "direction": "vertical" @@ -76,7 +125,8 @@ } ], "direction": "horizontal", - "width": 309.5 + "width": 309.5, + "collapsed": true }, "right": { "id": "bc4b945ded1926e3", @@ -188,16 +238,20 @@ "companion:Toggle completion": false } }, - "active": "9247ae5d7ced22e9", + "active": "fbeaa35cc5a8abf1", "lastOpenFiles": [ - "HCIW/slides/Gestural interaction.pdf", + "Concurrent Systems/slides/class 11.pdf", + "Concurrent Systems/notes/11 - LTSs and Bisimulation.md", + "Pasted image 20250414082824.png", + "Concurrent Systems/notes/12.md", + "Concurrent Systems/slides/class 12.pdf", + "HCIW/notes/3 - Beacons.md", "HCIW/slides/Zooming interfaces.pdf", + "HCIW/slides/Gestural interaction.pdf", "Concurrent Systems/notes/images/Pasted image 20250408091924.png", "Concurrent Systems/notes/images/Pasted image 20250408093840.png", "Concurrent Systems/notes/images/Pasted image 20250408094749.png", "Concurrent Systems/notes/images/Pasted image 20250408092853.png", - "Concurrent Systems/notes/11 - LTSs and Bisimulation.md", - "Concurrent Systems/slides/class 11.pdf", "Concurrent Systems/notes/10 - Implementing Consensus.md", "Concurrent Systems/notes/2 - Fast mutex by Lamport.md", "Concurrent Systems/notes/4 - Semaphores.md", @@ -215,7 +269,6 @@ "Concurrent Systems/a.md", "Concurrent Systems/notes/images/Pasted image 20250404235033.png", "Concurrent Systems/notes/images/Pasted image 20250304093223.png", - "Concurrent Systems/notes/Untitled.md", "Concurrent Systems/notes/9 - Consensus.md", "Concurrent Systems/notes/8 - Enhancing Liveness Properties.md", "Concurrent Systems/notes/7- MUTEX-free concurrency.md", @@ -226,16 +279,12 @@ "Concurrent.md", "Concurrent Systems/ignore this folder/Untitled.md", "Foundation of data science/notes/9 XGBoost.md", - "Foundation of data science/notes/9 Random Forest.md", "HCIW/slides/1 Interface and Interaction for IoT.pdf", "Concurrent Systems/slides/class 4.pdf", "Foundation of data science/class 9.pdf", "Concurrent Systems/slides/class 10.pdf", "Concurrent Systems/ignore this folder", - "HCIW/slides/Tangible User Interfaces.pdf", "Concurrent Systems/notes/images/Pasted image 20250401083747.png", - "Concurrent Systems/notes/images/Pasted image 20250401092557.png", - "Concurrent Systems/slides/class 6.pdf", "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 84fff64..6c60605 100644 --- a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md +++ b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md @@ -55,3 +55,9 @@ q0 is simulated by p0; this is shown by the following simulation relation: $$S = 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). +**Remark:** for proving equivalence, it is NOT enough to find a simulation of p by q and a simulation of q by p +![](../../Pasted%20image%2020250414082824.png) + +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 \ No newline at end of file diff --git a/Concurrent Systems/notes/12.md b/Concurrent Systems/notes/12.md new file mode 100644 index 0000000..e69de29 diff --git a/Concurrent Systems/slides/class 12.pdf b/Concurrent Systems/slides/class 12.pdf new file mode 100644 index 0000000..48b271d Binary files /dev/null and b/Concurrent Systems/slides/class 12.pdf differ diff --git a/Pasted image 20250414082824.png b/Pasted image 20250414082824.png new file mode 100644 index 0000000..294fd81 Binary files /dev/null and b/Pasted image 20250414082824.png differ