From 61b8f365553d3cf35cf03e4dc167c1b414733f8d Mon Sep 17 00:00:00 2001
From: Marco Realacci <marco@marcorealacci.me>
Date: Wed, 30 Apr 2025 17:28:22 +0200
Subject: [PATCH] vault backup: 2025-04-30 17:28:22

---
 Concurrent Systems/notes/13 - Weak Bisimilarity.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Concurrent Systems/notes/13 - Weak Bisimilarity.md b/Concurrent Systems/notes/13 - Weak Bisimilarity.md
index 601dd1d..6aeeb61 100644
--- a/Concurrent Systems/notes/13 - Weak Bisimilarity.md	
+++ b/Concurrent Systems/notes/13 - Weak Bisimilarity.md	
@@ -117,3 +117,8 @@ basically we need to have an initially habilitated process, which can be any (th
 This will generate the LTS:
 ![500](../../Pasted%20image%2020250430171336.png)
 
+Is the implementation correct w.r.t. the given specification? Yes.
+Weak bisimilarity $L \approx L_{i}$
+$$R \triangleq \{ (L, L_{i})\space|\space 0<i\leq n\} \space \cup \space \{\bar{p_{i}}.L,L'_{i} \space | \space 0<i<n  \}$$
+is a bisimulation, trust me bro.
+