master-degree-notes/Concurrent Systems/notes/13 - Weak Bisimilarity.md

The equivalence studied up to now is quite discriminating, in the sense that it distinguishes, for example, τ.P and τ.τ.P.

• If an external observer can count the number of non-observable actions (i.e., the τ’s), this distinction makes sense.
• If we assume that an observer cannot access any internal information of the system, then this distinction is not acceptable.

The idea of the new equivalence is to ignore (some) τ’s:

• a visible action must be replied to with the same action, possibly together with some internal actions
• an internal action must be replied to by a (possibly empty) sequence of internal actions.

We define the relation \implies as:

P \implies P' if and only if there exist P_{0}, P_{1},\dots,P_{k} (for k \geq 0) such that P=P_{0} \xrightarrow{\tau} P_{1} \xrightarrow{\tau}\dots\xrightarrow{\tau}Pk=P'

relation \xRightarrow{\hat{\alpha}}:

• if \alpha=\tau then \xRightarrow{\hat{\alpha}}\triangleq\implies
• otherwise \xRightarrow{\hat{\alpha}}\triangleq\implies\xrightarrow{\alpha}\implies

S is a weak simulation if and only if \forall(p, q) \in S \space \forall p \xrightarrow{\alpha} p' \exists q' \space s.t. \space q\xRightarrow{\hat{\alpha}}q' \space and \space (p', q') \in S A relation S is called weak bisimulation if both S and S^{-1} are weak simulations. We say that p and q are weakly bisimilar, written p \approx q, if there exists a weak bisimulation S such that (p, q) \in S.

Prop: \approx is a

1. equivalence
2. congruence
3. weak bisimulation
4. \sim \subset \approx

Examples of weakly bisimilar processes

Theorem: given any process P and any sum M, N, then:

1. P \approx \tau.{P}
2. M+N+\tau.N \approx M + \tau.N
3. M+\alpha.P+\alpha.(N+\tau.P) \approx M + \alpha.(N + \tau.P)

Proof: take the symmetric closure of the following relations, that can be easily shown to be weak simulations:

1. S = \{ (P,\tau.P )\}\cup Id
2. S=\{ (M+N+\tau.N,M+\tau.N )\}\cup Id
3. S=\{ ((M+\alpha.P+\alpha.(N+\tau.P), M+\alpha.(N+\tau.P)) \} \cup Id

Weak bisimilarity abstracts from any \tau

There exists no weak bisimulation S that contains (P, Q). Proof: By contr. suppose that a bisimulation exists Since Q −τ→ b.0, there must exist a P’ such that P ⇒ P and (P,b.0) ∈ S The only P that satisfies P ⇒ P’ is P itself hence it should be (P,b.0) ∈ S

Contradiction: P can perform a whereas b.0 cannot !! Similarly, P/R and Q/R are NOT weakly bisimilar

EXAMPLE: Factory

A factory can handle three kinds of works: easy (E), medium (M), difficult (D).

An activity of the factory consists in receiving in input a work (of any kind) and in producing in output a manufactured work.

The given specification of an activity is the following:

A\triangleq i_{E}.A'+i_{M}. A'+i_{D}.A'

A' \triangleq \bar{o}.A

where actions i_{E}, i_{M}, i_{D} represents they input, and \bar{o} represents the production of an output.

The factory is given by the parallel composition of two activities:

Factory \triangleq A|A

A possible implementation of this specification is obtained by having two workers that perform in parallel different kinds of work.

• For easy works, they don’t use any machinery
• For medium works, they can use either a special or a general machine
• For difficult works, they have to use the special machine. There is only one special and only one general machine that the workers have to share.

where rg and rs are used to require the general/special machine, lg and ls are used to leave the general/special machine, and S and G implement a semaphore on the two different machines.

The resulting system is given by:

Workers \triangleq (W|W|G|S) \setminus_{\{rg,rs,lg,ls  \}}

We now want to show that:

Factory \approx Workers

i.e., that the specification and the implementation of the factory behave the same (apart from internal actions).

Let N denote {rg,rs,lg,ls} and x,y ∊ {E,M,D} We can prove that the following relation is a weak bisimulation:

This is a family of relations:

• 3 pairs of the second form (one for every x)
• 9 pairs of the fifth form (one for every x and y)
• 3 pairs of the sixth form
• 3 pairs of the seventh form

Furthermore, we should also consider commutativity of parallel in pairs of the second, third, fourth, sixth, seventh and eighth form.

Thus, R is actually made up of 1+6+2+2+9+6+6+2 = 34 pairs. exercise: write down the LTSs