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

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

Browse source
This commit is contained in:
Marco Realacci 2025-04-30 19:33:22 +02:00
parent a01b48cc7c
commit 9a670602e9
2 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

5
.obsidian/workspace.json vendored
View file

@ -192,10 +192,10 @@
}, },
"active": "ec8d1a91f1f0cc7e", "active": "ec8d1a91f1f0cc7e",
"lastOpenFiles": [ "lastOpenFiles": [
"Pasted image 20250430192526.png", "Concurrent Systems/notes/12b - CCS cose varie.md",
"Concurrent Systems/notes/13 - Weak Bisimilarity.md", "Concurrent Systems/notes/13 - Weak Bisimilarity.md",
"Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md", "Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md",
"Concurrent Systems/notes/12b - CCS cose varie.md", "Pasted image 20250430192526.png",
"Concurrent Systems/notes/12 - Calculus of communicating system.md", "Concurrent Systems/notes/12 - Calculus of communicating system.md",
"Concurrent Systems/notes/11 - LTSs and Bisimulation.md", "Concurrent Systems/notes/11 - LTSs and Bisimulation.md",
"Concurrent Systems/notes/10 - Implementing Consensus.md", "Concurrent Systems/notes/10 - Implementing Consensus.md",
@ -210,7 +210,6 @@
"Concurrent Systems/notes/images/Pasted image 20250429092055.png", "Concurrent Systems/notes/images/Pasted image 20250429092055.png",
"Concurrent Systems/notes/images/Pasted image 20250429091959.png", "Concurrent Systems/notes/images/Pasted image 20250429091959.png",
"Concurrent Systems/notes/images/Pasted image 20250429091029.png", "Concurrent Systems/notes/images/Pasted image 20250429091029.png",
"Concurrent Systems/notes/images/Pasted image 20250429085319.png",
"Concurrent Systems/slides/class 12.pdf", "Concurrent Systems/slides/class 12.pdf",
"HCIW/slides/HCI in the car.pdf", "HCIW/slides/HCI in the car.pdf",
"Concurrent Systems/slides/class 11.pdf", "Concurrent Systems/slides/class 11.pdf",

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

@ -49,7 +49,10 @@ $P$ is in standard form if and only if $P \triangleq \sum_{i}\alpha_{i}P_{i}$ an
![](../../Pasted%20image%2020250430192526.png) ![](../../Pasted%20image%2020250430192526.png)
and eventually we find $P'$ which is literally the standard form of $P_{1}|P_{2}$. and eventually we find $P'$ which is literally the standard form of $P_{1}|P_{2}$.
2. $P \triangleq \sum_{i \in I}\alpha_{i}P_{i}$. By induction $\forall P_{i} \exists P_{i}$ 2. $P \triangleq \sum_{i \in I}\alpha_{i}P_{i}$. By induction $\forall P_{i} \exists P_{i}'$ in a standard form s.t. $\vdash P_{1}=P_{1}'$
Let's now consider a context: $\alpha_{1}.☐ + \sum_{i \in I}\alpha_{i}P_{i}$
Now we fill the context 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}'$
![](images/Pasted%20image%2020250429084921.png) ![](images/Pasted%20image%2020250429084921.png)
![](images/Pasted%20image%2020250429084950.png) ![](images/Pasted%20image%2020250429084950.png)
replacing one by one every continuation with its standard form, obtaining standard form. replacing one by one every continuation with its standard form, obtaining standard form.