AbstractA categorical definition of bisimulation, applicable to a wide range of models in concurrency with an accompanying notion af observations, was recently suggested by Joyal, Nielsen and Winskel. The definition is in terms of span of open maps, and it coincides with Park and Milner's strong bisimulation for the standard model of labelled transition systems with sequential observations. Here, we briefly present the general set-up, and discuss its applications. For the model of transition systems with independence and nonsequential observations, the associated notion of bisimulation was shown to be a slight strengthening of the history preserving bisimulations of Rabinovich and Trakhtenbrot. Furthermore, it turns out that this bisimulation has game theoretic and logical characterizations in the form of pleasantly simple modifications of well- known characterizations of standard strong bisimulation.
Categories and Subject Descriptors: F.1.2 [Computation by Abstract Devices]: Modes of Computation; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic
Additional Key Words and Phrases: concurrency, bisimulation, games, logics
Selected references
- Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137-161, January 1985.