63 lines
3 KiB
Markdown
63 lines
3 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
|
|
|
|
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
|
|
- ...
|
|
|
|
|
|
|
|
|
|
$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.
|
|
|
|
|
|
|
|
|
|
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:
|
|
|
|
|
|
|