vault backup: 2025-04-15 16:15:01

.obsidian/workspace.json

@@ -8,7 +8,7 @@
         "type": "tabs",
         "children": [
           {
-            "id": "84845736e00d5c98",
+            "id": "fc3ff5f9792d4a40",
             "type": "leaf",
             "state": {
               "type": "markdown",
@@ -20,8 +20,37 @@
               "icon": "lucide-file",
               "title": "12 - Calculus of communicating system"
             }
+          },
+          {
+            "id": "9d3f25b0eb9b478f",
+            "type": "leaf",
+            "state": {
+              "type": "markdown",
+              "state": {
+                "file": "Concurrent Systems/notes/12b - CCS cose varie.md",
+                "mode": "source",
+                "source": false
+              },
+              "icon": "lucide-file",
+              "title": "12b - CCS cose varie"
+            }
+          },
+          {
+            "id": "a222ab88db5cfdd0",
+            "type": "leaf",
+            "state": {
+              "type": "markdown",
+              "state": {
+                "file": "Concurrent Systems/notes/12b - CCS cose varie.md",
+                "mode": "source",
+                "source": false
+              },
+              "icon": "lucide-file",
+              "title": "12b - CCS cose varie"
+            }
           }
-        ]
+        ],
+        "currentTab": 2
       }
     ],
     "direction": "vertical"
@@ -78,8 +107,7 @@
       }
     ],
     "direction": "horizontal",
-    "width": 309.5,
-    "collapsed": true
+    "width": 309.5
   },
   "right": {
     "id": "bc4b945ded1926e3",
@@ -174,7 +202,8 @@
       }
     ],
     "direction": "horizontal",
-    "width": 364.5
+    "width": 364.5,
+    "collapsed": true
   },
   "left-ribbon": {
     "hiddenItems": {
@@ -190,13 +219,17 @@
       "companion:Toggle completion": false
     }
   },
-  "active": "0d5325c0f9289cea",
+  "active": "a222ab88db5cfdd0",
   "lastOpenFiles": [
-    "Concurrent Systems/notes/11 - LTSs and Bisimulation.md",
     "Concurrent Systems/notes/12 - Calculus of communicating system.md",
+    "Concurrent Systems/notes/11 - LTSs and Bisimulation.md",
+    "Concurrent Systems/notes/10 - Implementing Consensus.md",
+    "Concurrent Systems/notes/12b - CCS cose varie.md",
+    "Concurrent Systems/slides/class 12.pdf",
+    "Pasted image 20250415090109.png",
+    "Pasted image 20250415082906.png",
     "Concurrent Systems/notes/images/Pasted image 20250414164549.png",
     "Concurrent Systems/notes/images/Pasted image 20250414181443.png",
-    "Concurrent Systems/slides/class 12.pdf",
     "Concurrent Systems/slides/class 11.pdf",
     "Concurrent Systems/notes/images/Pasted image 20250414173011.png",
     "Concurrent Systems/notes/images/Pasted image 20250414082824.png",
@@ -204,12 +237,9 @@
     "Concurrent Systems/notes/images/Pasted image 20250414152247.png",
     "Concurrent Systems/notes/images/Pasted image 20250414152234.png",
     "Concurrent Systems/notes/images/Pasted image 20250414152221.png",
-    "Concurrent Systems/notes/images/Pasted image 20250414104010.png",
-    "Concurrent Systems/notes/images/Pasted image 20250414103800.png",
     "HCIW/notes/3 - Beacons.md",
     "HCIW/slides/Zooming interfaces.pdf",
     "HCIW/slides/Gestural interaction.pdf",
-    "Concurrent Systems/notes/10 - Implementing Consensus.md",
     "Concurrent Systems/notes/2 - Fast mutex by Lamport.md",
     "Concurrent Systems/notes/4 - Semaphores.md",
     "Concurrent Systems/notes/4b - Monitors.md",
@@ -231,7 +261,6 @@
     "Concurrent Systems/notes/6a - Alternatives to Atomicity.md",
     "Concurrent.md",
     "Concurrent Systems/ignore this folder/Untitled.md",
-    "Foundation of data science/notes/9 XGBoost.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/notes/12b - CCS cose varie.md

@@ -0,0 +1,69 @@
+An n-ary semaphore S(n)(p,v) is a process used to ensure that there are no more than n istances of the same activity concurrently in execution. An activity is started by action p and is terminated by action v.
+
+The specification of a unary semaphore is the following:
+$$S^{(1)} \triangleq p \cdot S_{1}^{(1)}$$
+$$S_{1}^{(1)} \triangleq p \cdot S_{}^{(1)}$$
+The specification of a binary semaphore is the following:
+$$S_{}^{(2)} \triangleq p \cdot S_{1}^{(2)}$$
+$$S_{1}^{(2)} \triangleq p \cdot S_{2}^{(2)}+v\cdot S^{(2)}$$
+$$S_{2}^{(2)} \triangleq v \cdot S_{1}^{(2)}$$
+
+If we consider S(2) as the specification of the expected behavior of a binary semaphore and S(1) | S(1) as its concrete implementation, we can show that $$S^{(1)}|S^{(1)} \space \textasciitilde \space S^{2}$$
+This means that the implementation and the specification do coincide. To show this equivalence, it suffices to show that following relation is a bisimulation:
+![](../../Pasted%20image%2020250415082906.png)
+
+## Restrictions
+**Proposition:** $a.P \textbackslash a ∼ 0$
+*Proof:*
+- S = {(a.P\a , 0)} is a bisimulation
+
+Which challenges can (a.P)\a have?
+- a.P can only perform a (and become P)
+- however, because of restriction, a.P\a is stuck
+
+ No challenge from a.P\a, nor from 0 -> bisimilar!
+
+**Proposition:** $\bar{a}.P \textbackslash a ∼ 0$
+*Proof is similar.*
+
+## Idempotency of Sum
+**Proposition:** $α.P+α.P+M ∼ α.P+M$
+*Proof:*
+$$S = \{ (α.P+α.P+M , α.P+M) \}$$
+Is it a bisimulation?
+NO: the problem is that, for example:
+- α.P+α.P+M –α–> P
+- α.P+M –α–> P
+- BUT (P,P) in general does NOT belong to S!
+
+So we can try with $$S = \{ (α.P+α.P+M , α.P+M) \} ∪ \{(P,P)\}$$
+But it is not yet a bisimulation.
+P –β–> P’ (challenge and reply), but we don't have (P', P') in S.
+
+So let's try with: $$S = \{ (α.P+α.P+M , α.P+M) \} ∪ Id$$
+Let's go!
+
+## Congruence
+One of the main aims of an equivalence notion between processes is to make equational reasonings of the kind: “if P and Q are equivalent, then they can be interchangeably used in any execution context”.
+
+This feature on an equivalence makes it a *congruence*
+Not all equivalences are necessarily congruences (even though most of them are).
+To properly define a congruence, we first need to define an execution context, and then what it means to run a process in a context. Intuitively:
+![200](../../Pasted%20image%2020250415090109.png)
+
+where C is a context (i.e., a process with a hole ☐), P is a process, and $C[P]$ denotes filling the hole with P
+
+Example: $$if \space C = (☐ | Q) \textbackslash a, \space then \space C[P] = (P | Q) \textbackslash a$$
+The set C of CCS contexts is given by the following grammar:
+$$C ::= ☐ \space | \space C|P \space | \space C \textbackslash a \space | \space a.C + M$$
+where M denotes a sum.
+
+An equivalence relation $R$ is a congruence if and only if
+$$\forall (P, Q) \in R, \forall C.(C[P], C[Q]) \in R$$
+Is bisimilarity a congruence? Yes.
+**Theorem:**
+$$if \space P ∼ Q \space then \space \forall C.C[P] ∼ C[Q]$$
+
+Proof on the slides.
+
+So today we learned that bisimulation is a good equivalence.