From 12f2215a1821d4cf88294a4ffa985790a1cbdd4c Mon Sep 17 00:00:00 2001
From: Marco Realacci <marco@marcorealacci.me>
Date: Tue, 15 Apr 2025 08:40:18 +0200
Subject: [PATCH] vault backup: 2025-04-15 08:40:18

---
 Concurrent Systems/notes/13 -.md | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

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