diff --git a/Concurrent Systems/notes/13 -.md b/Concurrent Systems/notes/13 -.md index 3f11c4c..c638f11 100644 --- a/Concurrent Systems/notes/13 -.md +++ b/Concurrent Systems/notes/13 -.md @@ -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: ![](../../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:** \ No newline at end of file