On Bisimilarities Induced by Relations on Actions

In this paper, we give a straightforward generalization of bisimulations to "bisimulations induced by a pair of relations" on the underlying action set. We establish that many of the nice properties of bisimulations and bisimilarities may be thought of as actually being inherited from properties of the underlying relations on actions. We show that many bisimulation-based orderings (including strong and weak bisimilarity) defined in the literature are instances of this generalization. We also show by an example that there are instances where the equivalence of two systems (which intuitively have the same functionality), cannot be established directly by observational equivalence, but requires a more general notion. We finally give an adaptation of the "on-the-fly algorithm " of Fernandez and Mourner for computing generalized bisimilarities