Available as compressed postscript (772k).
In this dissertation we investigate presheaf models for concurrent
computation. Our aim is to provide a systematic treatment of bisimulation
for
a wide range of concurrent process calculi. Bisimilarity is
defined abstractly in terms of open maps as in the work of
Joyal, Nielsen and Winskel.
Their work inspired this thesis by suggesting that presheaf
categories could provide abstract models for concurrency with a built-in notion
of bisimulation.
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, pi-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 finer 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 lambda-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.
@PhDthesis{cattani:thesis,
author = {Cattani, Gian Luca},
title = {Presheaf Models for Concurrency},
institution= {University of Aarhus},
year = {1999}
}