Go backward to
Strong Congruence
Go up to
Top
Go forward to
Weak Bisimulation and Observation Equivalence
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
n
and
E
->
alpha
_1
...->
alpha
_n
E'
.
E
=>
t
E'
if
t=
alpha
1
...
alpha
n
and
E
(->
tau
)
*
->
alpha
_1
(->
tau
)
*
...(->
tau
)
*
->
alpha
_n
(->
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