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

vault backup: 2025-04-15 08:40:18

Browse source
This commit is contained in:
Marco Realacci 2025-04-15 08:40:18 +02:00
parent 3e2dc34e61
commit 12f2215a18
1 changed files with 12 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

13
Concurrent Systems/notes/13 -.md
View file

@ -12,4 +12,15 @@ If we consider S(2) as the specification of the expected behavior of a binary se
This means that the implementation and the specification do coincide. To show this equivalence, it suffices to show that following relation is a bisimulation: This means that the implementation and the specification do coincide. To show this equivalence, it suffices to show that following relation is a bisimulation:
![](../../Pasted%20image%2020250415082906.png) ![](../../Pasted%20image%2020250415082906.png)
## Congruence ## Restrictions
**Proposition:** a.P\a ∼ 0
*Proof:*
- S = {(a.P\a , 0)} is a bisimulation
Which challenges can (a.P)\a have?
- a.P can only perform a (and become P)
- however, because of restriction, a.P\a is stuck
No challenge from a.P\a, nor from 0 à bisimilar!
**Proposition:**