Towards the unification of models for concurrency

Abstract

The problem of the conceptual unification of the models for concurrent and distributed systems is addressed in terms of categories of graphs with algebraic structure. In this paper, we model the semantics of a concrete process description language, in both its interleaving and its true concurrency versions. As a test case, we consider Mitner’s Calculus of Communicating Systems (CCS). Instead of defining a single model for CCS, we introduce categories whose objects are models, and where morphisms represent a specification-implementation relation. We start by showing that CCS models can be viewed as ordinary graphs equipped with additional structures over nodes and transitions. Labels are defined using a comma category construction. We then define special classes of morphisms expressing a notion of simplification and we show that observational congruences can be characterized in terms of final universal properties in the sub categories induced by such morphisms. In order to model the truly concurrent aspect of CCS, we write axioms which identify computations obtained by permuting independent transitions. By unfolding the resulting transition system, we obtain the domain of configurations of an event structure.