I'm pleased to announce that the following Ph.D. dissertation is now being distributed as a technical report and is available for download. -James Leifer INRIA Rocquencourt ================================================================= Author: James J. Leifer Title: ``Operational congruences for reactive systems'' Distribution: Ph.D. Dissertation and Technical Report 521, Computer Laboratory, University of Cambridge Supervisor: Robin Milner URL: http://pauillac.inria.fr/~leifer/ Abstract: The dynamics of process calculi, e.g. CCS, have often been defined using a labelled transition system (LTS). More recently it has become common when defining dynamics to use reaction rules ---i.e. unlabelled transition rules--- together with a structural congruence. This form, which I call a reactive system, is highly expressive but is limited in an important way: LTSs lead more naturally to operational equivalences and preorders. So one would like to derive from reaction rules a suitable LTS. This dissertation shows how to derive an LTS for a wide range of reactive systems. A label for an agent (process) a is defined to be any context F which intuitively is just large enough so that the agent Fa (``a in context F'') is able to perform a reaction. The key contribution of my work is the precise definition of ``just large enough'', in terms of the categorical notion of relative pushout (RPO), which ensures that several operational equivalences and preorders (strong bisimulation, weak bisimulation, the traces preorder, and the failurespreorder) are congruences when sufficient RPOs exist. I present a substantial example of a family of reactive systems based on closed, shallow action calculi (those with no free names and no nesting). I prove that sufficient RPOs exist for a category of such contexts. The proof is carried out indirectly in terms of a category of graphs and embeddings and gives precise (necessary and sufficient) conditions for the existence of RPOs. I conclude by arguing that these conditions are satisfied for a wide class of reaction rules. The thrust of this dissertation is, therefore, towards easing the burden of exploring new models of computation by providing a general method for achieving useful operational congruences. ================================================================= 10-Sep-2001 18:04:02 -0300,1686;000000000000-00000010