Bisimulation from Open Maps

André Joyal; Mogens Nielsen; Glynn Winskel

doi:10.1006/inco.1996.0057

Bisimulation from Open Maps

André Joyal, Mogens Nielsen, Glynn Winskel

Publikation: Bidrag til tidsskrift/Konferencebidrag i tidsskrift /Bidrag til avis › Tidsskriftartikel › Forskning › peer review

Abstract

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.

Originalsprog	Engelsk
Tidsskrift	Information and Computation
Vol/bind	127
Nummer	2
Sider (fra-til)	164-185
ISSN	0890-5401
DOI	https://doi.org/10.1006/inco.1996.0057
Status	Udgivet - 1996

Adgang til dokumentet

10.1006/inco.1996.0057

Citationsformater

@article{7b251b90f16311dfa891000ea68e967b,

title = "Bisimulation from Open Maps",

abstract = "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.",

author = "Andr{\'e} Joyal and Mogens Nielsen and Glynn Winskel",

note = "Also published in the BRICS Research Series as RS-94-7",

year = "1996",

doi = "10.1006/inco.1996.0057",

language = "English",

volume = "127",

pages = "164--185",

journal = "Information and Computation",

issn = "0890-5401",

publisher = "Academic Press",

number = "2",

}

TY - JOUR

T1 - Bisimulation from Open Maps

AU - Joyal, André

AU - Nielsen, Mogens

AU - Winskel, Glynn

N1 - Also published in the BRICS Research Series as RS-94-7

PY - 1996

Y1 - 1996

N2 - 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.

AB - 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.

U2 - 10.1006/inco.1996.0057

DO - 10.1006/inco.1996.0057

M3 - Journal article

SN - 0890-5401

VL - 127

SP - 164

EP - 185

JO - Information and Computation

JF - Information and Computation

IS - 2

ER -

Bisimulation from Open Maps

Abstract

Adgang til dokumentet

Fingeraftryk

Citationsformater