marcorealacci/master-degree-notes
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

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

Browse source
This commit is contained in:
Marco Realacci 2025-04-14 16:30:00 +02:00
parent 7012b24996
commit e29d303ef6
1 changed files with 2 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -49,7 +49,6 @@ $$\frac{P\{a_1/x_1, \dots, a_n/x_n\} \xrightarrow{\alpha} P'}{A(a_1, \dots, a_n)
##### 3. **Restriction (Hiding)** ##### 3. **Restriction (Hiding)**
$$\frac{P \xrightarrow{\alpha} P'}{P \setminus a \xrightarrow{\alpha} P' \setminus a} \quad \text{if } \alpha \notin \{a, \bar{a}\}$$ $$\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. > 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**
@ -60,21 +59,12 @@ $$\frac{P_1 \xrightarrow{\alpha} P_1'}{P_1 \mid P_2 \xrightarrow{\alpha} P_1' \m
###### b. **Right process makes a move:** ###### b. **Right process makes a move:**
$$\frac{P_2 \xrightarrow{\alpha} P_2'}{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'}$$
> Symmetrical to the previous: `P₂` makes the move. > Symmetrical to the previous: `P₂` makes the move.
--- ###### c. **Synchronization rule (communication):**
$$\frac{P_1 \xrightarrow{a} P_1' \quad P_2 \xrightarrow{\bar{a}} P_2'}{P_1 \mid P_2 \xrightarrow{\tau} P_1' \mid P_2'}$$
#### 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. > 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: ## 🧠 Summary Table:
|Rule Type|Description| |Rule Type|Description|