vault backup: 2025-04-14 18:19:02
This commit is contained in:
parent
ef831cf444
commit
15d90be7a7
5 changed files with 14 additions and 45 deletions
|
|
@ -0,0 +1,189 @@
|
|||
- Up to now, we have considered non-deterministic processes
|
||||
- Two main features are missing for modeling a concurrent system:
|
||||
- Simultaneous execution of processes
|
||||
- Inter-process interaction
|
||||
|
||||
- Solutions adopted:
|
||||
- Parallel composition, with interleaving semantics
|
||||
- Producer/consumer paradigm
|
||||
|
||||
>[!note] Suggested reading
|
||||
>https://en.wikipedia.org/wiki/Calculus_of_communicating_system
|
||||
|
||||
Given a set of names N (that denote events)
|
||||
- $a (\in N)$ denotes consumption of event a
|
||||
- $\bar{a}$ (for $a \in N$) denotes production of event a
|
||||
- $a$ and $\bar{a}$ are complementary actions: they let two parallel processes synchronize on the event a
|
||||
|
||||
When two processes synchronize, an external observer has no way of understanding what is happening in the system
|
||||
- synchronization is not observable from the outside; it produces a special ‘silent’ action, that we denote with τ
|
||||
The set of actions we shall consider is: $N \cup \bar{N} \cup \{\tau\}$
|
||||
|
||||
It is also useful to force some processes of the system to synchronize between them (without the possibility of showing to the outside some actions)
|
||||
|
||||
The restriction operator P\a restricts the scope of name a to process P (a is visible only from within P)
|
||||
|
||||
This is similar to local variables in a procedure of an imperative program
|
||||
|
||||
The set of CCS processes is defined by the following grammar:
|
||||
$$P::=\sum_{i \in I} \alpha _{i}.P_{i} \space |\space A(a_{1}\dots a
|
||||
_{n})\space|\space P|Q \space | \space P\setminus a$$
|
||||
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 / 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)**
|
||||
$${\sum_{i \in I} \alpha_i . P_i \xrightarrow{\alpha_j} P_j} \quad \text{for all } j \in I$$
|
||||
|
||||
> 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)**
|
||||
$$\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**
|
||||
There are three rules here for different situations in `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:**
|
||||
$$\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.
|
||||
|
||||
###### 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'}$$
|
||||
> 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 τ |
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
fino alla 7 compresa...
|
||||
|
||||
Sure Marco! Let's go step-by-step through the **CCS process transition example** in the figure, using:
|
||||
|
||||
- **Markdown for explanations**
|
||||
|
||||
- **LaTeX in Obsidian format** (with `$$...$$`) for math
|
||||
|
||||
|
||||
---
|
||||
|
||||
#### Example
|
||||
|
||||
|
||||
#### Example, but explained
|
||||
##### 📘 Definitions
|
||||
We start with the following **process definitions**:
|
||||
- $A \triangleq a.A'$
|
||||
- $A' \triangleq \bar{b}.A$
|
||||
- $B \triangleq b.B'$
|
||||
- $B' \triangleq \bar{c}.B$
|
||||
|
||||
Our **initial process** is: $A \mid B$
|
||||
##### ▶️ Step 1: Transition from A
|
||||
From the definition:
|
||||
|
||||
- $A \triangleq a.A'$
|
||||
- So we can do: $A \xrightarrow{a} A'$ (A consumes a and becomes A')
|
||||
|
||||
Using the **parallel rule** for the left-hand side:
|
||||
$$\frac{A \xrightarrow{a} A'}{A \mid B \xrightarrow{a} A' \mid B}$$
|
||||
✅ **First transition:** $A \mid B \xrightarrow{a} A' \mid B$
|
||||
|
||||
##### ▶️ Step 2: Synchronization: $\bar{b}$ and $b$
|
||||
We now have:
|
||||
- Left process: $A' \triangleq \bar{b}.A$
|
||||
- Right process: $B \triangleq b.B'$
|
||||
|
||||
From this, we can do:
|
||||
- $A' \xrightarrow{\bar{b}} A$
|
||||
- $B \xrightarrow{b} B'$
|
||||
|
||||
These actions **complement each other**, so we can apply the **synchronization rule**:
|
||||
|
||||
$$\frac{A' \xrightarrow{\bar{b}} A \quad B \xrightarrow{b} B'}{A' \mid B \xrightarrow{\tau} A \mid B'}$$
|
||||
|
||||
✅ **Second transition:**
|
||||
$$A' \mid B \xrightarrow{\tau} A \mid B'$$
|
||||
|
||||
##### ▶️ Step 3: Transition from B'
|
||||
From the definition:
|
||||
- $B' \triangleq \bar{c}.B$
|
||||
- So: $B' \xrightarrow{\bar{c}} B$
|
||||
|
||||
Now use the **right parallel rule**:
|
||||
$$\frac{B' \xrightarrow{\bar{c}} B}{A \mid B' \xrightarrow{\bar{c}} A \mid B}$$
|
||||
✅ **Third transition:**
|
||||
$$A \mid B' \xrightarrow{\bar{c}} A \mid B$$
|
||||
##### Synchronization
|
||||
In the image above, we can observe a τ-transition due to synchronization between two complementary actions, in fact:
|
||||
- A' produces b and becomes A
|
||||
- B consumes b and becomes B'
|
||||
|
||||
Since $\bar{b}$ and $b$ are complementary actions, they can **synchronize**, resulting in a **silent action** $\tau$ (synchronization rule):
|
||||
$$\frac{A' \xrightarrow{\bar{b}} A \quad B \xrightarrow{b} B'}{A' \mid B \xrightarrow{\tau} A \mid B'}$$
|
||||
|
||||
### LTS and parallelism
|
||||
In the construction of the LTS we loose the consciousness of the parallel
|
||||
- it is indeed possible, by having the new set of actions, to obtain the previous LTS through the syntax we considered last class.
|
||||
|
||||
The usefulness of the parallel is two-fold:
|
||||
- it is the fundamental operator in concurrency theory
|
||||
- it allows for a compact and intuitive writing of processes.
|
||||
|
||||
|
||||
### Restriction
|
||||
What if we restrict on b?
|
||||
|
||||
|
||||
|
||||
##### Example 1:
|
||||
since $a$ is not in $\{b, \bar{b}\}$, we will see the transitions:
|
||||
$$
|
||||
\frac{\frac{\frac{a.A' \xrightarrow{a} A' \quad A \triangleq a.A'}{A \xrightarrow{a} A'}}
|
||||
{{A \mid B \xrightarrow{a} A' \mid B}}a \not \in \{b, \bar{b}\}}{{(A \mid B) \setminus b \xrightarrow{a} (A' \mid B) \setminus b}}
|
||||
$$
|
||||
|
||||
Split in separate peaces for better readability:
|
||||
$$\frac{a.A' \xrightarrow{a} A' \quad A \triangleq a.A'}{A \xrightarrow{a} A'}
|
||||
\quad
|
||||
\frac{A \xrightarrow{a} A'}{A \mid B \xrightarrow{a} A' \mid B}
|
||||
\quad
|
||||
\frac{A \mid B \xrightarrow{a} A' \mid B \quad a \notin \{b, \bar{b}\}}{(A \mid B) \setminus b \xrightarrow{a} (A' \mid B) \setminus b}$$
|
||||
|
||||
##### Example 2:
|
||||
since $b$ is in $\{b, \bar{b}\}$, we will NOT see the transitions:
|
||||
$$\frac{\frac{\frac{b.B' \xrightarrow{b} B' \quad B \triangleq b.B'}{B \xrightarrow{b} B'}}
|
||||
{{A \mid B \xrightarrow{b} A \mid B'}}b \in \{b, \bar{b}\}}{{(A \mid B) \setminus b}}$$
|
||||
This time I won't split it in separate pieces since I don't feel like doing it, just buy glasses.
|
||||
|
||||
###### So... What if we restrict on b?
|
||||
- The effect of the restriction on b is that we have deleted the transitions involving b (hide all transitions labelled with $b$ and $\bar{b}$).
|
||||
- Notice that the τ, even if it has been generated by synchronizing on b, it is still present after applying the restriction on b!
|
||||
- the purpose of the τ is exactly to signal that a synchronization has happened but to hide the event on which the involved processed synchronized.
|
||||
|
||||
- In general, it is possible that whole states disappear upon restriction of some names: this would be the case, e.g., if we consider the LTS arising from $(A’ | B)\setminus a,b$ (restricting on both a and b):
|
||||
Loading…
Add table
Add a link
Reference in a new issue