Gian Luca Cattani
April 1999
We show how presheaf categories, in which
traditional models of concurrency are embedded, can be used to deduce
congruence properties of bisimulation for the traditional models. A key
result is given here; it is shown that the homomorphisms between presheaf
categories, i.e., colimit preserving functors, preserve open map
bisimulation. We follow up by observing that presheaf categories and colimit
preserving functors organise in what can be considered as a category of
non-deterministic domains. Presheaf models can be obtained as solutions to
recursive domain equations. We investigate properties of models given for a
range of concurrent process calculi, including CCS, CCS with
value-passing, -calculus and a form of CCS with linear process
passing. Open map bisimilarity is shown to be a congruence for each calculus.
These are consequences of general mathematical results like the preservation
of open map bisimulation by colimit preserving functors. In all but the case
of the higher order calculus, open map bisimulation is proved to coincide
with traditional notions of bisimulation for the process terms. In the case
of higher order processes, we obtain a ner equivalence than the one one would
normally expect, but this helps reveal interesting aspects of the
relationship between the presheaf and the operational semantics. For a
fragment of the language, corresponding to a form of
-calculus, open
map bisimulation coincides with applicative bisimulation.
In developing a suitable general theory of domains, we extend results and notions, such as the limit-colimit coincidence theorem of Smyth and Plotkin, from the order-enriched case to a ``fully'' 2-categorical situation. Moreover we provide a domain theoretical analysis of (open map) bisimulation in presheaf categories. We present, in fact, induction and coinduction principles for recursive domains as in the works of Pitts and of Hermida and Jacobs and use them to derive a coinduction property based on bisimulation
Available as PostScript,
PDF.