From 4e8e16e924e47066a4c377427259429461e4b820 Mon Sep 17 00:00:00 2001
From: Marco Realacci <marco@marcorealacci.me>
Date: Mon, 28 Apr 2025 08:37:04 +0200
Subject: [PATCH] vault backup: 2025-04-28 08:37:04

---
 .obsidian/workspace.json                           |  4 ++--
 Concurrent Systems/notes/13 - Weak Bisimilarity.md | 13 ++++++++++++-
 2 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json
index ade353f..5315cd8 100644
--- a/.obsidian/workspace.json
+++ b/.obsidian/workspace.json
@@ -213,9 +213,9 @@
   },
   "active": "56150e6df7869900",
   "lastOpenFiles": [
-    "Concurrent Systems/notes/12 - Calculus of communicating system.md",
-    "Concurrent Systems/notes/13 - Weak Bisimilarity.md",
     "Concurrent Systems/slides/class 13.pdf",
+    "Concurrent Systems/notes/13 - Weak Bisimilarity.md",
+    "Concurrent Systems/notes/12 - Calculus of communicating system.md",
     "Concurrent Systems/slides/class 12.pdf",
     "Concurrent Systems/notes/12b - CCS cose varie.md",
     "Concurrent Systems/notes/11 - LTSs and Bisimulation.md",
diff --git a/Concurrent Systems/notes/13 - Weak Bisimilarity.md b/Concurrent Systems/notes/13 - Weak Bisimilarity.md
index 73de9e7..2f7406f 100644
--- a/Concurrent Systems/notes/13 - Weak Bisimilarity.md	
+++ b/Concurrent Systems/notes/13 - Weak Bisimilarity.md	
@@ -13,4 +13,15 @@ $P \implies P'$ if and only if there exist $P_{0}, P_{1},\dots,P_{k}$ (for $k \g
 
 relation $\xRightarrow{\hat{\alpha}}$:
 - if $\alpha=\tau$ then $\xRightarrow{\hat{\alpha}}\triangleq\implies$
-- otherwise $\xRightarrow{\hat{\alpha}}\triangleq\implies\xrightarr$
\ No newline at end of file
+- otherwise $\xRightarrow{\hat{\alpha}}\triangleq\implies\xrightarrow{\alpha}\implies$
+
+S is a weak simulation if and only if $$\forall(p, q) \in S \space \forall p \xrightarrow{\alpha} p' \exists q' \space s.t. \space q\xRightarrow{\hat{\alpha}}q' \space and \space (p', q') \in S$$
+A relation S is called weak bisimulation if both $S$ and $S^{-1}$ are weak simulations.
+We say that p and q are weakly bisimilar, written $p \approx q$, if there exists a weak bisimulation $S$ such that $(p, q) \in S$.
+
+**Prop:**
+$\approx$ is a
+1. equivalence
+2. congruence
+3. weak bisimulation
+4. $\sim a$
\ No newline at end of file