Bisimulation from Open Maps

An abstract definition of bisimulation is presented. It makes possible a uniform definition of bisimulation across a range of different models for parallel computation presented as categories. As examples, transition systems, synchronisation trees, transition systems with independence (an abstraction from Petri nets), and labelled event structures are considered. On transition systems the abstract definition readily specialises to Milner's strong bisimulation. On event structures it explains and leads to a strengthening of the history-preserving bisimulation of Rabinovitch and Traktenbrot and van Glabeek and Goltz. A tie-up with open maps in a (pre)topos, as they appear in the work of Joyal and Moerdijk, brings to light a new model, presheaves on categories of pomsets, into which the usual category of labelled event structures embeds fully and faithfully. As an indication of its promise, this new presheaf model has “refinement” operators. The general approach yields a logic, generalising Hennessy–Milner logic, which is characteristic for the generalised notion of bisimulation.

Authors

• André Joyal
• Mogens Nielsen
• Glynn Winskel

Keywords

No keywords are indexed for this paper.