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

vault backup: 2025-04-27 23:00:45

Browse source
This commit is contained in:
Marco Realacci 2025-04-27 23:00:45 +02:00
parent 4116b92b5b
commit ef845edd98
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
Concurrent Systems/notes/12b - CCS cose varie.md
View file

@ -47,7 +47,7 @@ Let's go!
## Congruence ## Congruence
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”. 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* **This feature on an equivalence makes it a *congruence***
Not all equivalences are necessarily congruences (even though most of them are). 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: 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) ![200](../../Pasted%20image%2020250415090109.png)
@ -61,7 +61,7 @@ where M denotes a sum.
An equivalence relation $R$ is a congruence if and only if An equivalence relation $R$ is a congruence if and only if
$$\forall (P, Q) \in R, \forall C.(C[P], C[Q]) \in R$$ $$\forall (P, Q) \in R, \forall C.(C[P], C[Q]) \in R$$
Is bisimilarity a congruence? Yes. **Is bisimilarity a congruence? Yes.**
**Theorem:** **Theorem:**
$$if \space P ∼ Q \space then \space \forall C.C[P] ∼ C[Q]$$ $$if \space P ∼ Q \space then \space \forall C.C[P] ∼ C[Q]$$