marcorealacci/master-degree-notes
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

vault backup: 2025-04-30 20:03:22

Browse source
This commit is contained in:
Marco Realacci 2025-04-30 20:03:22 +02:00
parent 843d701ad8
commit 68e895e061
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md
View file

@ -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}$$ $$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\}$$ $$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})$$ 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 By using the same axiom to the parallel of the three processes, we obtain