From 149f35849b2516cd8eec5005b6bd384684449c22 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Wed, 30 Apr 2025 20:18:22 +0200 Subject: [PATCH] vault backup: 2025-04-30 20:18:22 --- .../notes/14 Checking bisimilarity, an inference system.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md b/Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md index 896e741..90cccf0 100644 --- a/Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md +++ b/Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md @@ -79,10 +79,10 @@ exercise: prove the weak bisimilarity between the spec and the implementation. Let us consider the parallel of processes M and R, by using the axiom for parallel, we have $$\vdash M|R=put.(\overline{go}|R)+go.(M|\overline{rcv})$$ By using the same axiom to the parallel of the three processes, we obtain $$\vdash S|(M|R)=send.(\overline{put}|(M|R))+put.(\overline{go}|R|S)+go.(\overline{rcv}|S|M)$$ -By restricting *put* and *go*, and by using the second axiom for restriction, we have that (spostiamo la res): +By restricting *put* and *go*, and by using the second axiom for restriction, we have that (spostiamo la restrizione dentro): ![](images/Pasted%20image%2020250429091959.png) -We now apply the third axiom for restriction to the three summands: +We now apply the third axiom for restriction to the three summands (effettivamente applichiamo la restrizione): ![](images/Pasted%20image%2020250429092055.png) ![](images/Pasted%20image%2020250429092305.png) ![](images/Pasted%20image%2020250429092543.png)