Weak Bisimulation and Open Maps

A general treatment of weak bisimulation and observation congruence on presheaf models is presented. It extends previous work on bisimulation from open maps and answers a fundamental question there. The consequences of the general theory are derived for two key models for concurrency, the interleaving model of synchronisation trees and the independence model of labelled event structures. Starting with a ``hiding'' functor from a category of paths to observable paths, it is shown how to derive a monad on the category of presheaves over the category of paths. The Kleisli category of the monad is shown to be equivalent to that of presheaves with weak morphisms, which roughly are only required to preserve observable paths. The monad is defined through an intermediary view of processes as bundles in Cat. This view, which seems important in its own right, leads directly to a hiding operation on processes; when the hiding operation is translated back to presheaves through an adjunction it yields the monad. The monad is shown to automatically preserve open-map bisimulation, generalising the expectation that strongly bisimilar processes should be weakly bisimilar. However, two alternative general ways to define weak bisimulation and observation congruence (in the Kleisli category itself or in the presheaf category after application of the monad) do not coincide in general. However a necessary and sufficient condition for their equivalence is proved; from this it is sufficient to show a fill-in condition applies to category of paths with weak morphisms. The fill-in condition is shown to hold for the two traditional models, synchronisation trees and event structures

Abstract: