2.6 KiB
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})