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 Milner'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.
Research supported in part by EEC Basic Research Action n. 3011 CEDISYS
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Benson, D. and Ben-Shachar, O. Bisimulations of Automata, Information and Computation, 79, 1988.
Boudol, G., Castellani, I. Concurrency and Atomicity. Theoret. Comput. Sci., 59, 1988.
Boudol, G., Castellani, I. Permutation of Transition: an Event Structure Semantics for CCS and SCCS, in Rex School/Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS 354, 1989
Bergstra, J., Klop, W. Process Algebra for Syncronous Communication. Information and Control, 60, 1984.
Brookes, S., Hoare, C.A.R., Roscoe, A. A Theory of Communicating Sequential Processes, Journal of ACM, 31, 3, 1984.
Casley, R., Crew, R., Meseguer, J., Pratt, W. Temporal Structures, in Third Symposium on Category Theory and Computer Science, LNCS 389, 1989.
Degano, P., De Nicola, R. Montanari, U. A Distributed Operational Semantics for CCS based on Condition/Event Systems. Acta Informatica, 26, 1988.
Degano, P., De Nicola, R. Montanari, U. A Partial Ordering Semantics for CCS, Technical Report TR-3/88, Dipartimento di Informatica, Università di Pisa, 1988 (To appear on Theoretical Computer Science)
Degano, P., Montanari, U. Concurrent Histories: A Basis for Observing Distributed Systems, Journal of Computer and System Sciences, 34, 1987, pp. 442–461.
Degano, P., Montanari, U., Meseguer, J. Axiomatizing Net Computations and Processes, In Proc Logics in Computer Science 89.
Ferrari, G. Unifying Models of Concurrency, PhD. Thesis, Dipartimento di Informatica, Università di Pisa, 1990.
Ferrari, G., Montanari, U. Strong and Weak Observational Congruences are Final Morphisms, Technical Report, Dipartimento di Informatica, Università di Pisa, 1990 (In preparation)
Ferrari, G., Montanari, U. Axiomatizing True Concurrency for CCS, Technical Report, Dipartimento di Informatica, Università di Pisa, 1990 (In preparation)
van Glabbeek, R., Goltz, U. Equivalence Notions for Concurrent Systems and Refinement of Actions, In MFCS'89, LNCS 379, 1989.
Gorrieri, R., Marchetti, S., Montanari, U. A2CCS: Atomic Actions for CCS, In Proc. CAAP 88, LNCS 299, 1988. Extended version to appear in Theoretical Computer Science.
Lambek, J., Scott P.J. Introduction to Higher Order Categorical Logic, Cambridge University Press, 1986.
Mac Lane, S. Categories for the Working Mathematicians, Springer-Verlag 1981
Meseguer, J. General Logics, in Logic Colloquium 87, North Holland
Meseguer, J., Montanari, U. Petri Nets are Monoids: A New Algebraic Foundation for Net Theory, In Proc Logics in Computer Science 88, 1988. Full version to appear Information and Computation
Milner, R. A Calculus of Communicating Systems, LNCS 92, 1980
Milner, R. Notes on a Calculus of Communicating Systems, in Control Flow, Data Flow: Concepts of Distributed Programming, (Broy Ed), NATO ASI Series F, Vol 14, Springer Verlag, 1985.
Montanari, U., Yankelevich, D. An Algebraic View of Interleaving and Distributed Operational Semantics, in Third Symposium on Category Theory and Computer Science, LNCS 389, 198
Nielsen, M., Plotkin G., Winskel, G. Petri Nets, Event Structures and Domains, Partl. Theoretical Computer Science, 13, 1981.
Park, D. Concurrency and Automata on Infinite Sequences, In Proc. GI, LNCS 104, 1981.
Plotkin, G. A Structured Approach to Operational Semantics, DAIMI FN-19, Computer Science Dept., Aarhus University, 1981
Pratt, V. Modelling Concurrency with Partial Orders, International Journal of Parallel Programming, 15, 1986, pp. 33–71.
Reisig, W. Petri Nets: an Introduction. EATCS Monographs, Springer-Verlag, 1985
Winskel, G. Event Structure Semantics of CCS and related Languages, In Proc ICALP 82, LNCS 140, 1982
Winskel, G. Event Structures Invited lecture for the Advanced Course on Petri Nets, LNCS 255, 1987
Winskel, G. An Introduction to Event Structures, in in Rex School/Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS 354, 1989
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ferrari, G.L., Montanari, U. (1990). Towards the unification of models for concurrency. In: Arnold, A. (eds) CAAP '90. CAAP 1990. Lecture Notes in Computer Science, vol 431. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52590-4_47
Download citation
DOI: https://doi.org/10.1007/3-540-52590-4_47
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52590-5
Online ISBN: 978-3-540-47042-7
eBook Packages: Springer Book Archive