117 lines
No EOL
5.8 KiB
Markdown
117 lines
No EOL
5.8 KiB
Markdown
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)$$
|
||
basically we need to have an initially habilitated process, which can be any (the first one in our case).
|
||
|
||
This will generate the LTS: |