DocumentCode
1822293
Title
Bisimulation and open maps
Author
Joyal, Andre ; Nielson, M. ; Winskel, Glynn
Author_Institution
Dept. de Math. et d´´Inf., UQAM, Montreal, Que., Canada
fYear
1993
fDate
19-23 Jun 1993
Firstpage
418
Lastpage
427
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
Keywords
Petri nets; category theory; formal logic; parallel processing; simulation; Petri nets; abstract definition; categories; history-preserving bisimulation; independence; labeled event structures; open maps; parallel computation; pomsets; presheaf model; presheaves; pretopos; refinement operators; strong bisimulation; synchronization trees; transition systems; Computational modeling; Concurrent computing; History; Interleaved codes; Logic; Petri nets;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 1993. LICS '93., Proceedings of Eighth Annual IEEE Symposium on
Conference_Location
Montreal, Que.
Print_ISBN
0-8186-3140-6
Type
conf
DOI
10.1109/LICS.1993.287566
Filename
287566
Link To Document