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

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

@@ -39,36 +39,22 @@ Dove:
 
 #### 📜 Inference rules
 ##### 1. **Choice (Summation Rule)**
+$${\sum_{i \in I} \alpha_i . P_i \xrightarrow{\alpha_j} P_j} \quad \text{for all } j \in I$$
 
-**$$∑_{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'`**
+> A process that has multiple options (`α₁.P₁ + α₂.P₂ + ...`) can non-deterministically choose any one of them.
 
+##### 2. **Process Definition (Call/Expansion)**
+$$\frac{P\{a_1/x_1, \dots, a_n/x_n\} \xrightarrow{\alpha} P'}{A(a_1, \dots, a_n) \xrightarrow{\alpha} P'} \quad A(x_1, \dots, x_n) \triangleq 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`**
+##### 3. **Restriction (Hiding)**
+$$\frac{P \xrightarrow{\alpha} P'}{P \setminus a \xrightarrow{\alpha} P' \setminus a} \quad \text{if } \alpha \notin \{a, \bar{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**
-
+##### 4. **Parallel Composition – Independent Actions**
+$$\frac{P_1 \xrightarrow{\alpha} P_1'}{P_1 \mid P_2 \xrightarrow{\alpha} P_1' \mid P_2}$$
+$$\frac{P_2 \xrightarrow{\alpha} P_2'}{P_1 \mid P_2 \xrightarrow{\alpha} P_1 \mid P_2'}$$
 There are three rules here for different situations in `P₁ | P₂`.
 
 ---