diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 69c3e6f..0dd4358 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -4,39 +4,19 @@ "type": "split", "children": [ { - "id": "4f1f4ad35c07ecf2", + "id": "67c0c397411f4359", "type": "tabs", "children": [ { - "id": "40e3ec35e1961dd0", - "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": "bfb7d80a61762b38", - "type": "tabs", - "children": [ - { - "id": "ba09b8276acab4c7", + "id": "9247ae5d7ced22e9", "type": "leaf", "state": { "type": "pdf", "state": { - "file": "Concurrent Systems/slides/class 11.pdf" + "file": "HCIW/slides/Gestural interaction.pdf" }, "icon": "lucide-file-text", - "title": "class 11" + "title": "Gestural interaction" } } ] @@ -96,8 +76,7 @@ } ], "direction": "horizontal", - "width": 309.5, - "collapsed": true + "width": 309.5 }, "right": { "id": "bc4b945ded1926e3", @@ -209,14 +188,15 @@ "companion:Toggle completion": false } }, - "active": "40e3ec35e1961dd0", + "active": "9247ae5d7ced22e9", "lastOpenFiles": [ - "Concurrent Systems/slides/class 11.pdf", + "Concurrent Systems/notes/images/Pasted image 20250408091924.png", + "HCIW/slides/Gestural interaction.pdf", + "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", - "Pasted image 20250408094749.png", - "Pasted image 20250408093840.png", - "Pasted image 20250408092853.png", - "Pasted image 20250408091924.png", + "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", @@ -255,7 +235,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/slides/class 8.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 5e65655..84fff64 100644 --- a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md +++ b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md @@ -12,13 +12,13 @@ Automata Behaviour: language equivalence >[!note] Language equivalence >M1 and M2 are *language equivalent* if and only if L(M1)=L(M2) -![](../../Pasted%20image%2020250408091924.png) +![](images/Pasted%20image%2020250408091924.png) By considering the starting states as also final, they both generate the same language, i.e.: $$(20.(tea + 20.coffee))∗ = (20.tea + 20.20.coffee)∗$$ But, do they behave the same from the point of view of an external observer?? -![](../../Pasted%20image%2020250408092853.png) +![](images/Pasted%20image%2020250408092853.png) The essence of the difference is WHEN the decision to branch is taken - language equivalence gets rid of branching points - it is too coarse for our purposes! @@ -38,7 +38,7 @@ We shall usually write s –a–> s′ instead of ⟨s,a,s′⟩ ∈ T. ### Bisimulation Intuitively, two states are equivalent if they can perform the same actions that lead them in states where this property still holds -![](../../Pasted%20image%2020250408093840.png) +![](images/Pasted%20image%2020250408093840.png) P0 and Q0 are different because, after an a, the former can decide to do b or c, whereas the latter must decide this before performing a. Let (Q,T) be an LTS. @@ -50,7 +50,7 @@ We say that S is a bisimulation if both S and S−1 are simulations (where $$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) +![](images/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). diff --git a/Pasted image 20250408091924.png b/Concurrent Systems/notes/images/Pasted image 20250408091924.png similarity index 100% rename from Pasted image 20250408091924.png rename to Concurrent Systems/notes/images/Pasted image 20250408091924.png diff --git a/Pasted image 20250408092853.png b/Concurrent Systems/notes/images/Pasted image 20250408092853.png similarity index 100% rename from Pasted image 20250408092853.png rename to Concurrent Systems/notes/images/Pasted image 20250408092853.png diff --git a/Pasted image 20250408093840.png b/Concurrent Systems/notes/images/Pasted image 20250408093840.png similarity index 100% rename from Pasted image 20250408093840.png rename to Concurrent Systems/notes/images/Pasted image 20250408093840.png diff --git a/Pasted image 20250408094749.png b/Concurrent Systems/notes/images/Pasted image 20250408094749.png similarity index 100% rename from Pasted image 20250408094749.png rename to Concurrent Systems/notes/images/Pasted image 20250408094749.png diff --git a/HCIW/slides/Gestural interaction.pdf b/HCIW/slides/Gestural interaction.pdf new file mode 100644 index 0000000..3fe400f Binary files /dev/null and b/HCIW/slides/Gestural interaction.pdf differ