vault backup: 2025-04-28 08:27:04

.obsidian/workspace.json

@@ -6,31 +6,39 @@
       {
         "id": "ceb8ca67f2b32f40",
         "type": "tabs",
+        "dimension": 40.83094555873926,
         "children": [
           {
-            "id": "fc3ff5f9792d4a40",
+            "id": "56150e6df7869900",
-            "type": "leaf",
-            "state": {
-              "type": "pdf",
-              "state": {
-                "file": "Concurrent Systems/slides/class 12.pdf"
-              },
-              "icon": "lucide-file-text",
-              "title": "class 12"
-            }
-          },
-          {
-            "id": "9d3f25b0eb9b478f",
             "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"
   ]
 }

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}$