78 lines
3.6 KiB
Markdown
78 lines
3.6 KiB
Markdown
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
|
|
just what we've seen so far, literally.
|
|
|
|
|
|
quite obvious.
|
|
|
|
|
|
basically we can let the left or the right process evolve, leaving the other unchanged, or they can synchronize.
|
|
|
|
|
|
- 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
|
|
|
|
|
|
- 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$, we need to consider the relation $\{ LHS,RHS \} \cup Id$ and prove it's a bisimulation (spoiler: it is).
|
|
|
|
Since bisimilarity is an equivalence and a congruence, the inference rules holds.
|
|
|
|
|
|
>[!def] Standard form
|
|
$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 \space \exists \space 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.
|
|
|
|
|
|
|
|
|
|
replacing one by one every continuation with its standard form, obtaining standard form.
|
|
|
|
|
|
|
|
### Axioms & Rules for Weak Bisimilarity
|
|
|
|
|
|
#### 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:
|
|
|
|
|
|
We now apply the third axiom for restriction to the three summands:
|
|
|
|
|
|
|