diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 289607d..03137b5 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -6,31 +6,39 @@ { "id": "ceb8ca67f2b32f40", "type": "tabs", + "dimension": 40.83094555873926, "children": [ { - "id": "fc3ff5f9792d4a40", - "type": "leaf", - "state": { - "type": "pdf", - "state": { - "file": "Concurrent Systems/slides/class 12.pdf" - }, - "icon": "lucide-file-text", - "title": "class 12" - } - }, - { - "id": "9d3f25b0eb9b478f", + "id": "56150e6df7869900", "type": "leaf", "state": { "type": "markdown", "state": { - "file": "Concurrent Systems/notes/12 - Calculus of communicating system.md", + "file": "Concurrent Systems/notes/13 - Weak Bisimilarity.md", "mode": "source", "source": false }, "icon": "lucide-file", - "title": "12 - Calculus of communicating system" + "title": "13 - Weak Bisimilarity" + } + } + ] + }, + { + "id": "e6a32eeb8d1da29c", + "type": "tabs", + "dimension": 59.16905444126075, + "children": [ + { + "id": "6c4a39240e6da514", + "type": "leaf", + "state": { + "type": "pdf", + "state": { + "file": "Concurrent Systems/slides/class 13.pdf" + }, + "icon": "lucide-file-text", + "title": "class 13" } } ] @@ -90,7 +98,8 @@ } ], "direction": "horizontal", - "width": 309.5 + "width": 309.5, + "collapsed": true }, "right": { "id": "bc4b945ded1926e3", @@ -202,10 +211,12 @@ "companion:Toggle completion": false } }, - "active": "fc3ff5f9792d4a40", + "active": "56150e6df7869900", "lastOpenFiles": [ - "Concurrent Systems/notes/12 - Calculus of communicating system.md", + "Concurrent Systems/slides/class 13.pdf", + "Concurrent Systems/notes/13 - Weak Bisimilarity.md", "Concurrent Systems/slides/class 12.pdf", + "Concurrent Systems/notes/12 - Calculus of communicating system.md", "Concurrent Systems/notes/12b - CCS cose varie.md", "Concurrent Systems/notes/11 - LTSs and Bisimulation.md", "HCIW/slides/HCI in the car.pdf", @@ -244,11 +255,9 @@ "Concurrent Systems/notes/1 - CS Basics.md", "Concurrent Systems/notes/6a - Alternatives to Atomicity.md", "Concurrent.md", - "Concurrent Systems/ignore this folder/Untitled.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", "Senza nome.canvas" ] } \ No newline at end of file diff --git a/Concurrent Systems/notes/13 - Weak Bisimilarity.md b/Concurrent Systems/notes/13 - Weak Bisimilarity.md new file mode 100644 index 0000000..2adebed --- /dev/null +++ b/Concurrent Systems/notes/13 - Weak Bisimilarity.md @@ -0,0 +1,10 @@ +The equivalence studied up to now is quite discriminating, in the sense that it distinguishes, for example, τ.P and τ.τ.P. + +- If an external observer can count the number of non-observable actions (i.e., the τ’s), this distinction makes sense. +- If we assume that an observer cannot access any internal information of the system, then this distinction is not acceptable. + +The idea of the new equivalence is to ignore (some) τ’s: +- a visible action must be replied to with the same action, possibly together with some internal actions +- an internal action must be replied to by a (possibly empty) sequence of internal actions. + +$P \implies P'$ if and only if there exist $P_{0}, P_{1},\dots,P_{k}$ (for $k \geq 0$) such that $P=P_{0} \xrightarrow{\tau} P_{1} \xrightarrow{\tau}$ \ No newline at end of file diff --git a/Concurrent Systems/slides/class 13.pdf b/Concurrent Systems/slides/class 13.pdf new file mode 100644 index 0000000..06e7062 Binary files /dev/null and b/Concurrent Systems/slides/class 13.pdf differ