79 lines
No EOL
3.8 KiB
Markdown
79 lines
No EOL
3.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 \}}$$ |