[CST-2] Bisimulation

[Matej Pfajfar]

> Topics in Concurrency notes, p67.
> "We see that a binary relation $R$ between processes is a strong
> bisimulation iff $R \subseteq \varphi(R)$".
Well I wouldn't say obvious cos it took me a while to get comfortable with
it, but it's kind of intuitive.

If we define p phi(R) q to hold when the strong bisimulation conditions
hold then then phi(R) is a bisimulation (by definition).

But then if R is to be a bisimulation it must be a subset of phi(R).
I.e. R is a postfixed point of phi. That's how you then get R as a maximum
fixed point.

Hmm is that not intuitive? If it's not don't tell me cos I like thinking
that it is! ;-)

Matej

Matej Pfajfar
St John's College, University of Cambridge, UK

GPG Public Key @ http://matejpfajfar.co.uk/keys
Most people are good people, the rest of us are going to
run the world. -- badbytes

WARNING: THIS E-MAIL ACCOUNT WILL BE DELETED ON
         15/07/2002. PLEASE USE mp@cantab.net.