From c7b0b8e6b30e5326f1a236fcaaeb7473dc1b620a Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Mon, 28 Apr 2025 08:32:04 +0200 Subject: [PATCH] vault backup: 2025-04-28 08:32:04 --- .obsidian/workspace.json | 6 +++--- Concurrent Systems/notes/13 - Weak Bisimilarity.md | 8 +++++++- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 03137b5..ade353f 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -213,10 +213,10 @@ }, "active": "56150e6df7869900", "lastOpenFiles": [ - "Concurrent Systems/slides/class 13.pdf", - "Concurrent Systems/notes/13 - Weak Bisimilarity.md", - "Concurrent Systems/slides/class 12.pdf", "Concurrent Systems/notes/12 - Calculus of communicating system.md", + "Concurrent Systems/notes/13 - Weak Bisimilarity.md", + "Concurrent Systems/slides/class 13.pdf", + "Concurrent Systems/slides/class 12.pdf", "Concurrent Systems/notes/12b - CCS cose varie.md", "Concurrent Systems/notes/11 - LTSs and Bisimulation.md", "HCIW/slides/HCI in the car.pdf", diff --git a/Concurrent Systems/notes/13 - Weak Bisimilarity.md b/Concurrent Systems/notes/13 - Weak Bisimilarity.md index 2adebed..73de9e7 100644 --- a/Concurrent Systems/notes/13 - Weak Bisimilarity.md +++ b/Concurrent Systems/notes/13 - Weak Bisimilarity.md @@ -7,4 +7,10 @@ The idea of the new equivalence is to ignore (some) τ’s: - a visible action must be replied to with the same action, possibly together with some internal actions - an internal action must be replied to by a (possibly empty) sequence of internal actions. -$P \implies P'$ if and only if there exist $P_{0}, P_{1},\dots,P_{k}$ (for $k \geq 0$) such that $P=P_{0} \xrightarrow{\tau} P_{1} \xrightarrow{\tau}$ \ No newline at end of file +We define the relation $\implies$ as: + +$P \implies P'$ if and only if there exist $P_{0}, P_{1},\dots,P_{k}$ (for $k \geq 0$) such that $P=P_{0} \xrightarrow{\tau} P_{1} \xrightarrow{\tau}\dots\xrightarrow{\tau}Pk=P'$ + +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