diff --git a/Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md b/Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md index 51bef10..8d7d538 100644 --- a/Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md +++ b/Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md @@ -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 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! - -3. ![](images/Pasted%20image%2020250429085319.png) ### Axioms & Rules for Weak Bisimilarity ![](images/Pasted%20image%2020250429091029.png) +#### Completeness theorem: $P \sim Q \implies \vdash P=Q$ + + #### Example A server for exchanging messages, in its minimal version, receives a request for sending messages and delivers the confirmation of the reception