From f12ec7708612a12046cdc5134b2a5f3d0d1a5d6d Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Wed, 30 Apr 2025 19:13:22 +0200 Subject: [PATCH] vault backup: 2025-04-30 19:13:22 --- .../14 Checking bisimilarity, an inference system.md | 10 ++++++++++ 1 file changed, 10 insertions(+) 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 7e274b4..a4a4375 100644 --- a/Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md +++ b/Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md @@ -7,6 +7,8 @@ Inference system = axioms + inference rules - completeness: whatever is bisimilar, it can be inferred #### Axioms & Rules for Strong Bisimilarity +just what we've seen so far, literally. + ![350](images/Pasted%20image%2020250429082812.png) quite obvious. @@ -15,11 +17,19 @@ basically we can let the left or the right process evolve, leaving the other unc ![350](images/Pasted%20image%2020250429083129.png) - if a process does not perform any action, a restriction won't do anything +- restriction is distributive - if the process does not do the restricted action, the restriction won't do anything - what if we restrict on the actual action? - well, then the process becomes 0 ![350](images/Pasted%20image%2020250429083455.png) +- if $P = P \land P = Q => Q = P$ (it's transitive :o) +- the same happens with contexts + + +#### Soundness theorem: $\vdash P=Q \implies P \sim Q$ +*Proof:* +If $\vdash LHS=RHS$e need to consider the relation $\{ LHS,RHS \}$ ![](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.