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\xrightarr