Talk by Marco Hollenberg
General Safety for Bisimulation
In the literature several characterisations exist for first order formulas that
have certain properties with respect to bisimulation.
For instance, the first order formulas that are {\em invariant for bisimulation}
are precisely the modal formulas.
Another example is the characterisation of formulas that are {\em safe} for
bisimulation: this yields precisely the programs of PDL not using iteration.
The advent of modal logics built on top of first order languages containing
relations of any arity creates the need for a broader definition of bisimulation: it also obviates the need for new notions of safety for
bisimulation.
We present a characterisation theorem for these new notions.
The results dealing with invariance and safety are a consequence of the latter
characterisation.
Paul Dekker, November 2, 1995