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

4.5 KiB
Raw Blame History

  • 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

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) https://en.wikipedia.org/wiki/Calculus_of_communicating_system

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 its 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...