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

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

Browse source
This commit is contained in:
Marco Realacci 2025-04-30 20:13:22 +02:00
parent 68e895e061
commit 578c0bf0fc
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

@ -79,7 +79,7 @@ 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
$$\vdash S|(M|R)=send.(\overline{put}|(M|R))+put.(\overline{go}|R|S)+go.(\overline{rcv}|S|M)$$ $$\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: By restricting *put* and *go*, and by using the second axiom for restriction, we have that (spostiamo la res):
![](images/Pasted%20image%2020250429091959.png) ![](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: