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

vault backup: 2025-04-30 19:48:22

Browse source
This commit is contained in:
Marco Realacci 2025-04-30 19:48:22 +02:00
parent 31b548b632
commit a873734439
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -54,14 +54,15 @@ $P$ is in standard form if and only if $P \triangleq \sum_{i}\alpha_{i}P_{i}$ an
Now we fill the hole (*er bucio*) with $P_1$ and remove 1 from the set I (basically we pull it out from the summation): $$\alpha_{1}.P_{1} + \sum_{i \in I\setminus \{ 1 \}}\alpha_{i}P_{i}$$ Now we fill the hole (*er bucio*) with $P_1$ and remove 1 from the set I (basically we pull it out from the summation): $$\alpha_{1}.P_{1} + \sum_{i \in I\setminus \{ 1 \}}\alpha_{i}P_{i}$$
Now we replace $P_1$ with $P_{1}'$ and obtain: $$=\alpha_{1}.P_{1}' + \sum_{i \in I\setminus \{ 1 \}}\alpha_{i}P_{i}$$ Now we replace $P_1$ with $P_{1}'$ and obtain: $$=\alpha_{1}.P_{1}' + \sum_{i \in I\setminus \{ 1 \}}\alpha_{i}P_{i}$$
imagine doing this until you pulled everything out... Standard form! imagine doing this until you pulled everything out... Standard form!
3.
![](images/Pasted%20image%2020250429085319.png) ![](images/Pasted%20image%2020250429085319.png)
### Axioms & Rules for Weak Bisimilarity ### Axioms & Rules for Weak Bisimilarity
![](images/Pasted%20image%2020250429091029.png) ![](images/Pasted%20image%2020250429091029.png)
#### Completeness theorem: $P \sim Q \implies \vdash P=Q$
#### Example #### Example
A server for exchanging messages, in its minimal version, receives a request for sending messages and delivers the confirmation of the reception A server for exchanging messages, in its minimal version, receives a request for sending messages and delivers the confirmation of the reception