From a8737344399ad8e43796f6eebff7902f0b7fbe0d Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Wed, 30 Apr 2025 19:48:22 +0200 Subject: [PATCH] vault backup: 2025-04-30 19:48:22 --- .../notes/14 Checking bisimilarity, an inference system.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) 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