Go backward to
Bisimulation and Observation Equivalence
Go up to
Top
Go forward to
Examples
Weak Bisimulation and Observation Equivalence
(Weak) bisimulation
Binary relation
S
such that
(P,Q)
in
S
implies
if
P
->
alpha
P'
, then
Q
=>
alpha
^
Q'
with
(P',Q')
in
S
(and vice versa).
Observation equivalence
P
~~
Q
P
~~
Q
if
(P,Q)
in
S
for some weak bisimulation
S
.
~~ =
union
{
S
:
S
is a weak bisimulation}
Author:
Wolfgang Schreiner
Last Modification: June 8, 1998