41 lines
No EOL
2 KiB
Markdown
41 lines
No EOL
2 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+) \}$ |