vault backup: 2025-04-14 16:15:00

.obsidian/workspace.json

@@ -36,7 +36,8 @@
               "title": "12 - CCS (che non so cosa voglia dire)"
             }
           }
-        ]
+        ],
+        "currentTab": 1
       },
       {
         "id": "dd628773839aa478",
@@ -237,7 +238,7 @@
       "companion:Toggle completion": false
     }
   },
-  "active": "fbeaa35cc5a8abf1",
+  "active": "84845736e00d5c98",
   "lastOpenFiles": [
     "Concurrent Systems/slides/class 12.pdf",
     "Concurrent Systems/notes/12 - CCS (che non so cosa voglia dire).md",

Concurrent Systems/notes/12 - CCS (che non so cosa voglia dire).md

@@ -30,7 +30,93 @@ Dove:
 - **$\alpha _{i}.P_{i}$:** the process $P_{i}$ can perform the action $a$ and continue as the process $P_{i}$
 - $A(a_{1}\dots a_{n})$ parametric call to a process
 - $P|Q$ parallel composition: P and Q are in a concurrent execution and can communicate to each-other
-	- $P\setminus a$ as described before, is the process P without $a$ (the action is hidden / )
+- $P\setminus a$ as described before, is the process P without $a$ (the action is hidden / visible only internally by P)
+
+**Recap:**
+- `P ⟶ᵃ P'` means: _Process `P` can perform action `a` and become `P'`_
+- `α` is an action: input (`a`), output (`ā`), or internal (`τ`)
+- `{a₁/x₁, ..., aₙ/xₙ}` is a **substitution** (used in process definitions with parameters)
+
+#### 📜 Inference rules
+##### 1. **Choice (Summation Rule)**
+
+**$$∑_{i ∈ I} αᵢ.Pᵢ ⟶^{αⱼ} Pⱼ\space\space\spac, for \space all \space j \in I$$
+
+> A process that has multiple options (`α₁.P₁ + α₂.P₂ + ...`) can nondeterministically choose any one of them.
+
+---
+
+### 2. **Process Definition (Call/Expansion)**
+
+**`P{a₁/x₁ ... aₙ/xₙ} ⟶ᵅ P'`  
+`A(x₁...xₙ) ≜ P`  
+——————————————  
+`A(a₁...aₙ) ⟶ᵅ P'`**
+
+> If a process `A(x₁...xₙ)` is defined as `P`, then invoking `A(a₁...aₙ)` behaves like `P` with the arguments substituted.
+
+---
+
+### 3. **Restriction (Hiding)**
+
+**`P ⟶ᵅ P'` and `α ∉ {a, ā}`  
+——————————————  
+`P \ a ⟶ᵅ P' \ a`**
+
+> If process `P` can do action `α` and it’s **not** the hidden action (`a` or `ā`), then `P \ a` can also do it, and the resulting process remains restricted.
+
+---
+
+### 4. **Parallel Composition – Independent Actions**
+
+There are three rules here for different situations in `P₁ | P₂`.
+
+---
+
+#### a. **Left process makes a move:**
+
+**`P₁ ⟶ᵅ P₁'`  
+———————————  
+`P₁ | P₂ ⟶ᵅ P₁' | P₂`**
+
+> If `P₁` makes a move alone, the parallel composition can reflect it.
+
+---
+
+#### b. **Right process makes a move:**
+
+**`P₂ ⟶ᵅ P₂'`  
+———————————  
+`P₁ | P₂ ⟶ᵅ P₁ | P₂'`**
+
+> Symmetrical to the previous: `P₂` makes the move.
+
+---
+
+#### c. **Synchronization rule (communication):**
+
+**`P₁ ⟶ᵃ P₁'` and `P₂ ⟶ā P₂'`  
+——————————————  
+`P₁ | P₂ ⟶^τ P₁' | P₂'`**
+
+> If one process can **send** (`a`) and the other can **receive** (`ā`), they **synchronize**, and the result is an **internal (τ)** action. This models communication.
+
+---
+
+## 🧠 Summary Table:
+
+|Rule Type|Description|
+|---|---|
+|Choice|Select one summand to act|
+|Process Call|Expand definition by substituting parameters|
+|Restriction|Only allows transitions not involving the restricted action|
+|Parallel (independent)|A single component acts, the other stays the same|
+|Parallel (sync)|Two components synchronize to produce τ|
+
+---
+
+Let me know if you want to **trace an example** using these rules step-by-step — like watching how a CCS process evolves over time. It's super helpful to solidify the concepts!
+
 
 ![](images/Pasted%20image%2020250414104010.png)