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

vault backup: 2025-04-30 13:27:49

Browse source
This commit is contained in:
Marco Realacci 2025-04-30 13:27:49 +02:00
parent 1dd2d3df46
commit 0c758d98a2
25 changed files with 45 additions and 53 deletions
Download patch file Download diff file Expand all files Collapse all files

28
Concurrent Systems/notes/14.md
View file

@ -7,19 +7,19 @@ Inference system = axioms + inference rules
- completeness: whatever is bisimilar, it can be inferred
#### Axioms & Rules for Strong Bisimilarity
![350](../../Pasted%20image%2020250429082812.png)
![350](images/Pasted%20image%2020250429082812.png)
quite obvious.
![350](../../Pasted%20image%2020250429082905.png)
![350](images/Pasted%20image%2020250429082905.png)
basically we can let the left or the right process evolve, leaving the other unchanged, or they can synchronize.
![350](../../Pasted%20image%2020250429083129.png)
![350](images/Pasted%20image%2020250429083129.png)
- if a process does not perform any action, a restriction won't do anything
- ...
![350](../../Pasted%20image%2020250429083455.png)
![350](images/Pasted%20image%2020250429083455.png)
![](../../Pasted%20image%2020250429083535.png)
![](images/Pasted%20image%2020250429083535.png)
$P$ is in standard form if and only if $P \triangleq \sum_{i}\alpha_{i}P_{i}$ and $\forall_{i}P_{i}$ is in standard form.
**Lemma:** $\forall P \exists P'$* in standard form such that $\vdash P = P'$
@ -28,15 +28,15 @@ $P$ is in standard form if and only if $P \triangleq \sum_{i}\alpha_{i}P_{i}$ an
**Base case:** $P \triangleq 0$. It suffices to consider $P' \triangleq 0$ and conclude reflexivity.
**Inductive step:** we have to consider three cases.
![](../../Pasted%20image%2020250429084358.png)
![](../../Pasted%20image%2020250429084921.png)
![](../../Pasted%20image%2020250429084950.png)
![](images/Pasted%20image%2020250429084358.png)
![](images/Pasted%20image%2020250429084921.png)
![](images/Pasted%20image%2020250429084950.png)
replacing one by one every continuation with its standard form, obtaining standard form.
![](../../Pasted%20image%2020250429085319.png)
![](images/Pasted%20image%2020250429085319.png)
### Axioms & Rules for Weak Bisimilarity
![](../../Pasted%20image%2020250429091029.png)
![](images/Pasted%20image%2020250429091029.png)
#### Example
A server for exchanging messages, in its minimal version, receives a request for sending messages and delivers the confirmation of the reception
@ -55,9 +55,9 @@ Let us consider the parallel of processes M and R, by using the axiom for parall
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:
![](../../Pasted%20image%2020250429091959.png)
![](images/Pasted%20image%2020250429091959.png)
We now apply the third axiom for restriction to the three summands:
![](../../Pasted%20image%2020250429092055.png)
![](../../Pasted%20image%2020250429092305.png)
![](../../Pasted%20image%2020250429092543.png)
![](images/Pasted%20image%2020250429092055.png)
![](images/Pasted%20image%2020250429092305.png)
![](images/Pasted%20image%2020250429092543.png)