In: Albert, J.L.; et al.: Lecture Notes in Computer Science, Vol. 510; Proceedings of the 18th International Colloquium on Automata, Languages and Programming, 1991, Madrid, Spain, pages 495-505. Berlin, Germany: Springer-Verlag, 1991.
Abstract: History preserving bisimulation takes full account of the interplay between causality and branching, and it induces a congruence w.r.t. action refinement; but even for finite safe Petri nets it is based on a possibly infinite transition system. The paper introduces ordered markings of nets and the corresponding OM-bisimulation. It is shown that OM-bisimilarity coincides with history preserving bisimilarity, and that it can be decided for finite safe nets.
Keywords: history preserving bisimilarity; action refinement; decidability (of) ordered marking bisimulation; finite safe net.