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

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

Browse source
This commit is contained in:
Marco Realacci 2025-04-14 16:25:00 +02:00
parent 8357256efe
commit 7012b24996
1 changed files with 4 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -53,27 +53,13 @@ $$\frac{P \xrightarrow{\alpha} P'}{P \setminus a \xrightarrow{\alpha} P' \setmin
> 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**
$$\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₂`.
---
#### a. **Left process makes a move:**
**`P₁ ⟶ᵅ P₁'`
———————————
`P₁ | P₂ ⟶ᵅ P₁' | P₂`**
###### a. **Left process makes a move:**
$$\frac{P_1 \xrightarrow{\alpha} P_1'}{P_1 \mid P_2 \xrightarrow{\alpha} P_1' \mid P_2}$$
> If `P₁` makes a move alone, the parallel composition can reflect it.
---
#### b. **Right process makes a move:**
**`P₂ ⟶ᵅ P₂'`
———————————
`P₁ | P₂ ⟶ᵅ P₁ | P₂'`**
###### 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'}$$
> Symmetrical to the previous: `P₂` makes the move.