53 lines
No EOL
2.5 KiB
Markdown
53 lines
No EOL
2.5 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 |