Eighth Annual IEEE Symposium on

Logic in Computer Science (LICS 1993)

Paper: Bisimulation and open maps (at LICS 1993)

Authors: André Joyal Mogens Nielson Glynn Winskel

Abstract

An abstract definition of bisimulation is presented. It allows a uniform definition of bisimulation across a range of different models for parallel computation presented as categories. As examples, transition systems, synchronization trees, transition systems with independence (an abstraction from Petri nets), and labeled event structures are considered. On transition systems, the abstract definition readily specialises to Milner's (1989) strong bisimulation. On event structures, it explains and leads to a revision of the history-preserving bisimulation of Rabinovitch and Traktenbrot (1988), and Goltz and van Glabeek (1989). A tie-up with open maps in a (pre)topos brings to light a promising new model, presheaves on categories of pomsets, into which the usual category of labeled event structures embeds fully and faithfully. As an indication of its promise, this new presheaf model has refinement operators, though further work is required to justify their appropriateness and understand their relation to previous attempts

BibTeX

  @InProceedings{JoyalNielsonWinskel-Bisimulationandopen,
    author = 	 {André Joyal and Mogens Nielson and Glynn Winskel},
    title = 	 {Bisimulation and open maps},
    booktitle =  {Proceedings of the Eighth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1993},
    year =	 1993,
    editor =	 {Moshe Vardi},
    month =	 {June}, 
    pages =      {418--427},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }