From 8b82d461a0ba6929164f5ccaaa05c83cf02ee20b Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 29 Apr 2025 09:18:47 +0200 Subject: [PATCH] vault backup: 2025-04-29 09:18:47 --- Concurrent Systems/notes/14.md | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Concurrent Systems/notes/14.md b/Concurrent Systems/notes/14.md index e9f069c..95c203d 100644 --- a/Concurrent Systems/notes/14.md +++ b/Concurrent Systems/notes/14.md @@ -47,4 +47,10 @@ The behavior of such a server can be implemented by three processes in parallel: - another one effectively sends the message (through the restricted action *put*) and waits for the signal of message reception (through the restricted action *go*) - the last one gives back to the user the outcome of the sending -$$S \triangleq send.\overline{put} \quad M \triangleq send.\overline{put}$$ +$$S \triangleq send.\overline{put} \quad M \triangleq put.\overline{go} \quad R \triangleq go.\overline{rcv}$$ +$$Impl \triangleq (S|M|R)\setminus\{put, go\}$$ +exercise: prove the weak bisimilarity + +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})$$ \ No newline at end of file