vault backup: 2025-04-30 18:58:22

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

@@ -0,0 +1,63 @@
+We shall only consider finite processes (processes without recursive definitions)
+- a limited handling of recursion is possible
+- deciding bisimilarity for general processes is undecidable
+
+Inference system = axioms + inference rules
+- soundness: whatever I infer is correct (i.e., bisimiar)
+- completeness: whatever is bisimilar, it can be inferred
+
+#### Axioms & Rules for Strong Bisimilarity
+![350](images/Pasted%20image%2020250429082812.png)
+ quite obvious.
+
+![350](images/Pasted%20image%2020250429082905.png)
+basically we can let the left or the right process evolve, leaving the other unchanged, or they can synchronize.
+
+![350](images/Pasted%20image%2020250429083129.png)
+- if a process does not perform any action, a restriction won't do anything
+- ...
+
+![350](images/Pasted%20image%2020250429083455.png)
+
+![](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.
+
+**Lemma:** $\forall P \exists P'$* in standard form such that $\vdash P = P'$
+*Proof:* by induction on the structure of P.
+
+**Base case:** $P \triangleq 0$. It suffices to consider $P' \triangleq 0$ and conclude reflexivity.
+**Inductive step:** we have to consider three cases.
+
+![](images/Pasted%20image%2020250429084358.png)
+![](images/Pasted%20image%2020250429084921.png)
+![](images/Pasted%20image%2020250429084950.png)
+replacing one by one every continuation with its standard form, obtaining standard form.
+
+![](images/Pasted%20image%2020250429085319.png)
+
+### Axioms & Rules for Weak Bisimilarity
+![](images/Pasted%20image%2020250429091029.png)
+
+#### Example
+A server for exchanging messages, in its minimal version, receives a request for sending messages and delivers the confirmation of the reception
+
+Specification: $$Spec \triangleq send.\overline{rcv}$$
+The behavior of such a server can be implemented by three processes in parallel:
+- one handles the button for sending
+- another one effectively sends the message (through the restricted action *put*) and waits for the signal of message reception (through the restricted action *go*)
+- the last one gives back to the user the outcome of the sending
+
+$$S \triangleq send.\overline{put} \quad M \triangleq put.\overline{go} \quad R \triangleq go.\overline{rcv}$$
+$$Impl \triangleq (S|M|R)\setminus\{put, go\}$$
+exercise: prove the weak bisimilarity
+
+Let us consider the parallel of processes M and R, by using the axiom for parallel, we have $$\vdash M|R=put.(\overline{go}|R)+go.(M|\overline{rcv})$$
+By using the same axiom to the parallel of the three processes, we obtain
+$$\vdash S|(M|R)=send.(\overline{put}|(M|R))+put.(\overline{go}|R|S)+go.(\overline{rcv}|S|M)$$
+By restricting *put* and *go*, and by using the second axiom for restriction, we have that:
+![](images/Pasted%20image%2020250429091959.png)
+
+We now apply the third axiom for restriction to the three summands:
+![](images/Pasted%20image%2020250429092055.png)
+![](images/Pasted%20image%2020250429092305.png)
+![](images/Pasted%20image%2020250429092543.png)