A functorial semantics for observed concurrency
This paper presents a meta-model of observation in concurrency theory; it allows us to unify notions of observation in many different behavioural settings. We treat traces, process trees and event structures, and show how observations of them fit into a common framework. Behaviour and observation will both be modeled as categories and lined using the notions of ‘functor’ and ‘adjunction’.
Timing will be our chief example of observation; we present a timed traces model, and hint how it generalises to timed process trees (branching time) and timed ‘true concurrency.’ The general setup sees timing as a way of embedding observations into time; we propose stable categories of embeddings as natural metamodels of timed observation.
KeywordsStable Category Terminal Object Concurrency Theory Finite Distributive Lattice Functorial Semantic
Unable to display preview. Download preview PDF.
- 1.S. Abramsky and S. Vickers, Quantales, observationallogic and process semantics, Technical Report DOC 90/1, Department of Computing, Imperial College, 1991.Google Scholar
- 2.J. van Benthem, The logic of time, D. Reidel, 1983.Google Scholar
- 3.S. Brookes and A. Roscoe, An improved failures model for communicating sequential processes, in the Proceedings NSF-SERC Seminar on Concurrency, Volume 197, Springer-Verlag LNCS, 1985.Google Scholar
- 5.T. Coquand, C. Gunter, and G. Winskel, dI-domains as a model of polymorphism, in Mathematical Foundations of Programming Language Semantics, Volume 298, Springer-Verlag LNCS, 1988.Google Scholar
- 6.J. Davies and S. Schneider, An introduction to timed CSP, Technical Report Number 75, Oxford University Computer Laboratory, 1989.Google Scholar
- 7.U. Engberg and G. Winskel, Petri nets as models of linear logic, in the Proceedings of TAPSOFT (CAAP) (A. Arnold, Ed.), Volume 431, Springer-Verlag LNCS, 1990.Google Scholar
- 8.C. Hoare, Communicating sequential processes, International series on computer science, Prentice-Hall, 1985.Google Scholar
- 9.A. Jeffrey, Timed process algebra ≠ time × process algebra, Technical Report 79, Programming Methodology Group, Chalmers University, 1991.Google Scholar
- 10.J. Meseguer and U. Montanari, Petri nets are monoids: A new algebraic foundation for net theory, in Logic in Computer Science, (1988), 1988, Proceedings of the 3rd Annual IEEE Symposium, pp. 155–164.Google Scholar
- 11.D. Murphy, Time, causality, and concurrency, Ph.D. thesis, Department of Mathematics, University of Surrey, 1989, available as Technical Report CSC 90/R32, Department of Computing Science, University of Glasgow.Google Scholar
- 12.D. Murphy and A. Poigné, A functorial semantics for observed concurrency, Technical Report to appear, GMD, 1992.Google Scholar
- 13.A. Pnueli, Linear and branching structures in the semantics and logics of reactive systems, in Automata, Languages and Programming (W. Brauer, Ed.), Volume 194, Springer-Verlag LNCS, 1986, (12th Coll.).Google Scholar
- 14.S. Vickers, Topology via logic, Tracts in Theoretical Computer Science, Volume 5, Cambridge University Press, 1989.Google Scholar
- 15.G. Whitrow, The natural philosophy of time, Oxford University Press, 1980.Google Scholar
- 16.G. Winskel, Event structures, in Petri Nets: Central Models and Their Properties (W. Brauer, W. Reisig, and G. Rozenberg, Eds.), Volume 254, Springer-Verlag LNCS, 1986, Proceedings of Advances in Petri Nets. Also available as a Cambridge University Computer Laboratory Technical Report.Google Scholar