Bisimulation for reactive frames

Abstract

Reactive frames are those whose structure is not fi xed but can vary according to the path chosen. This kind of frame has been study and both a logic and an axiomatization for it were already developed. In this paper we take this study further and de fine a notion of bisimulation for reactive models. We show that the logic introduced by Marcelino for these frames is invariant under our notion of bisimulation. Finally, we proof the Hennessy-Milner theorem for a class of reactive models.