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

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

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

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

@ -41,4 +41,11 @@ But it is not yet a bisimulation.
P –β–> P’ (challenge and reply), but we don't have (P', P') in S. P –β–> P’ (challenge and reply), but we don't have (P', P') in S.
So let's try with: $$S = \{ (α.P+α.P+M , α.P+M) \} ∪ Id$$ So let's try with: $$S = \{ (α.P+α.P+M , α.P+M) \} ∪ Id$$
Let's go! Let's go!
## 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”.
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: