From 68e895e0615753f880160d4714b6054a71e51d84 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Wed, 30 Apr 2025 20:03:22 +0200 Subject: [PATCH] vault backup: 2025-04-30 20:03:22 --- .../notes/14 Checking bisimilarity, an inference system.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 1e8cd1d..730bbcb 100644 --- a/Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md +++ b/Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md @@ -74,7 +74,7 @@ The behavior of such a server can be implemented by three processes in parallel: $$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 +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