Presheaf Models for CCS-like Languages
Gian Luca Cattani
November 1999 |
Abstract:
The aim of this paper is to harness the mathematical machinery
around presheaves for the purposes of process calculi. Joyal, Nielsen and
Winskel proposed a general definition of bisimulation from open maps. Here we
show that open-map bisimulations within a range of presheaf models are
congruences for a general process language, in which CCS and related
languages are easily encoded. The results are then transferred to traditional
models for processes. By first establishing the congruence results for
presheaf models, abstract, general proofs of congruence properties can be
provided and the awkwardness caused through traditional models not always
possessing the cartesian liftings, used in the break-down of process
operations, are side-stepped. The abstract results are applied to show that
hereditary history-preserving bisimulation is a congruence for CCS-like
languages to which is added a refinement operator on event structures as
proposed by van Glabbeek and Goltz
Available as PostScript, PDF, DVI. |