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

vault backup: 2025-04-15 09:05:18

Browse source
This commit is contained in:
Marco Realacci 2025-04-15 09:05:18 +02:00
parent 60bcdfd382
commit 8dd45af905
3 changed files with 10 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

11
Concurrent Systems/notes/13 - CCS cose varie.md
View file

@ -47,5 +47,12 @@ Let's go!
One of the main aims of an equivalence notion between processes is to make equational reasonings of the kind: “if P and Q are equivalent, then they can be interchangeably used in any execution context”.
This feature on an equivalence makes it a *congruence*
Not all equivalences are necessarily congruences (even though most of them are
To properly define a congruence, we first need to define an execution context, and then what it means to run a process in a context. Intuitively:
Not all equivalences are necessarily congruences (even though most of them are).
To properly define a congruence, we first need to define an execution context, and then what it means to run a process in a context. Intuitively:
![200](../../Pasted%20image%2020250415090109.png)
where C is a context (i.e., a process with a hole ☐), P is a process, and $C[P]$ denotes filling the hole with P
Example: $$if \space C = (☐ | Q) \textbackslash a, \space then \space C[P] = (P | Q) \textbackslash a$$
The set C of CCS contexts is given by the following grammar:
$$C ::= ☐ \space | \space C|P \space | $$