Go backward to Strong CongruenceGo up to TopGo forward to Weak Bisimulation and Observation Equivalence |

- (Weak) bisimulation and (observation) equivalence:
`tau`action may be matched by zero or more`tau`actions.

- Auxiliary definitions:
*t*^ is the action sequence gained by deleting all occurences of`tau`from*t*.*E*->t^{}*E'*, if*t=*`alpha`..._{1}`alpha`and_{n}*E*->_1...->^{alpha}_n^{alpha}*E'*.*E*=>t^{}*E'*if*t=*`alpha`..._{1}`alpha`and_{n}*E*(->)^{tau}->^{*}_1(->^{alpha})^{tau}...(->^{*})^{tau}->^{*}_n(->^{alpha})^{tau}^{*}*E'*.*E'*is a*t*-descendant of*E*iff*E*=>t^{}*^**E'*.

- Relationship
*P*->t^{}*P'*implies*P*=>t^{}*P'*implies*P*->t^{}*^**P'*

Author: Wolfgang Schreiner

Last Modification: June 8, 1998