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

EXAMPLE: Lottery

We want to model a lottery L where we can select any ball from a bag that contains n balls; after every extraction, the extracted ball is put back in the bag and the procedure is repeated.

The specification is: L \triangleq \tau.\bar{p_{1}}L+\tau.\bar{p_{2}}.L+\dots+\tau.\bar{p_{n}}.L where $\tau$'s represent ball extractions and \tilde{p_{i}} is the action that communicates with the value of the extracted ball. The LTS resulting from this specification is:

We now build a system with n components, one for every ball.

Every component can be in three states:

• A (waiting for being habilitated to extraction)
• B (habilitated, with the possibility of being extracted or of habilitating the next component)
• C (extracted, waiting to externally communicate its value and start the process again): A_{i}=a_{i}.B_{i} \quad B_{i}=\tau.C_{i}+\bar{a}_{(i \space mod \space n)+1}.A_{i} \quad C_{i}=\bar{p}_{i}.B_{i} In pratica ogni volta o estrae di nuovo "se stesso" oppure "abilita" il componente successivo.

Implementation: Impl \triangleq (B_{1}|A_{2}|\dots|An)\setminus_{\{ a_{1}\dots an \}} basically we need to have an initially habilitated process, which can be any (the first one in our case).

This will generate the LTS:

Is the implementation correct w.r.t. the given specification? Yes. Weak bisimilarity L \approx L_{i}

R \triangleq \{ (L, L_{i})\space|\space 0<i\leq n\} \space \cup \space \{\bar{p_{i}}.L,L'_{i} \space | \space 0<i<n  \}

is a weak bisimulation, trust me bro.

EXAMPLE: Scheduler

We have a set of processes Pi (for 0 < i ≤ n) that must repeatedly perform at certain task.

A scheduler has to guarantee that processes cyclically start their task, starting from P1. Executions of different processes may overlap but the scheduler has to guarantee that every process Pi completes his performance before starting another one (with the same index i).

Every process Pi requires to start its task via action a_i and signals to the scheduler its termination via action b_i

• the scheduler has to guarantee that the a’s cyclically occur, starting with a_1, and, for every i, the ai’s must alternate with the bi’s, starting with a_i.

The specification is: if i \in X then:

S_{i,X}=\sum_{j \in X}b_{j}.S_{i,X-\{ j \}}

otherwise: S_{i,X}=a_{i}.S_{(i \space mod \space n)+1,X\cup \{ i \}} + \sum_{j \in X}b_{j}.S_{i,X-\{ j \}} Starting config S_{1,\{ \}} LTS for n=2:

We can try to implement the scheduler in the following way:

A_{i}=a_{i}.B_{i} \quad B_{i}=\bar{c}_{(i \space mod \space n)+1}.C_{i} \quad C_{i}=b_{i}.D_{i} \quad D_{i}=c_{i}.A_{i}

• actions of kind \bar{c} are needed to signal to the next process (i.e., with the next index) that it can start working
• actions of kind c are needed to receive from the previous process such a signal
  • such actions implement a token ring; the token is initially given to the first process: S=(A_{1}|D_{2}|\dots|D_{n})\setminus _{\{ c_{1}\dots cn \}}

Is the implementation correct? Or, in other words, S ≈ S_{1,∅}? No (ci sono rimasto male anche io).

Ma il fatto è che questo porta a questo LTS:

Il gioco (infamata incredibile comunque) sta nel fatto che con la restrizione per \{ c_{1},c_{2} \}, B_{2} non può evolvere in C_2 da solo, potrebbe farlo solo con una sincronizzazione! Che non c'è...

Fix: C_{i}=b_{i}.D_{i}+c_{i}.b_{i}.A_{i} in questo modo possiamo permettere al processo di ricevere c_{i} anche nello stato C, permettendo la sincronizzazione. In ogni caso tanto resterà in esecuzione finché non riceverà b_i.