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

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$e need to consider the relation \{ LHS,RHS \}

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: