Abstract
One of the main problems of the partial ordering approach to the description of computations of concurrent and distributed systems is that there is no operation of sequential composition for partial orders which preserves all information on causal dependencies (except for the simple case of series parallel pomsets). As a result, truly concurrent behavioural equivalences are defined by giving integral descriptions of computations: they are not obtained by composing the observations of the elementary steps of the computations. In this paper we introduce the algebra of Concatenable Concurrent Histories. A Concatenable Concurrent History describes a computation by means of a partial ordering of events together with information on the initial and final state of the computation. The operation of sequential conposition is one of the primitive operations of this algebra. We introduce a category of transition systems for CCS (called CCS models) and we show that in this category there exists a CCS model which has the structure of Concatenable Concurrent Histories. This object constitutes our model of observations. As a consequence our observations are incremental. The observation mechanism is handled by a labelling construction which is an internal operation of the category of models. Furthermore, we give a bisimulation congruence for CCS, via Concatenable Concurrent History observations, which can be characterized in terms of a final universal property in a suitable subcategory of CCS models. This category also provides a framework in which to interpret a Hennessy-Milner style programming logic which describes properties of the observable behaviour of computations. The equivalence naturally induced by the logic coincides with the congruence induced by the final object. This result expresses a sort of duality between semantic analysis based on observations and programming logics. We obtain an analogous result for a weaker congruence which results when internal actions are unobservable.
Research supported by, and collaboratively carried out at, Hewlett-Packard Laboratories, Pisa Science Centre, Corso Italia 114, 56125 Pisa, Italy.
Chapter PDF
Similar content being viewed by others
Keywords
- Operational Semantic
- Congruence Class
- Communicate Sequential Process
- Minimal Realization
- Causal Dependency
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abramsky, S., A Domain Equation for Bisimulation, Internal report, Dept. Computing, Imperial College
Arnold, A., Dicky, A., An Algebraic Characterization of Transition System Equivalences, Information and Computation 82, 1989.
Boudol, G., Castellani, I., Concurrency and Atomicity, Theoretical Computer Science 59, 1988.
Boudol, G., Castellani, I., Permutations of Transitions: An Event Structure Semantics for CCS, In Proc. REX School, Workshop on Linear Time, Branching Time, and Partial Orders in Logics and Models for Concurrency, LNCS 354, 1989.
Bergstra, J., Klop, W., Process Algebra for Synchronous Communication, Information and Control 60, 1984.
Darondeau, P., Degano, P. Causal Trees, In Proc. ICALP 89, LNCS 372, 1989.
Degano, P. De Nicola, R., Montanari, U. Observational Equivalences for Concurrency Models, in Formal Description of Programming Concepts III, M. Wirsing, ed., North Holland, 1987.
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. On the Consistency of Truly Concurrent Operational and Denotational Semantics. Proc. LICS 1988.
Degano, P. De Nicola, R., Montanari, U. Partial Ordering Descriptions and Observations of Nondeterministic Concurrent Processes, in Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS 354, 1987.
Degano, P. De Nicola, R., Montanari, U. A Partial Ordering Semantics for CCS, Theoretical Computer Science 75, 1990.
Degano, P., Meseguer, J., Montanari, U., Axiomatizing Net Computations and Processes, in Proc. Logics in Computer Science 89, 1989.
Degano, P., Montanari, U., Concurrent Histories: A Basis for Observing Distributed Systems, Journal of Computer and System Sciences 34, 1987.
De Nicola, R. Ferrari, G. Observational Logics and Concurrency Models, Proc 10th Conf. FST and TCS, LNCS 472, 1990
Ferrari, G. Unifying Models of Concurrency, PhD Thesis, TD/4-90, Dipartimento di Informatica, Univ. Pisa, 1990.
Ferrari, G., Montanari, U., Towards the Unification of Models for Concurrency, Proc. CAAP'90, LNCS 431, 1990.
Goltz, U. On Representing CCS Programs by Finite Petri Nets, Proc. MFCS 88, LNCS 324, 1988.
Goguen, J. Realization is Universal, Math. Systems Theory, 6, 1972.
Giarratana, V., Gimona, F., Montanari, U. Observability Concepts in Abstract Data Type Specifications, in Proc. MFCS 76, LNCS 45, 1976.
Gorrieri, R., Montanari, U., SCONE: a Simple Calculus of Nets, In Proc. CONCUR'90, LNCS 458, 1990.
Goltz, U., Reisig, W., The Non Sequential Behaviour of Petri Nets, Information and Computation 57, 1983.
Harel, D. Dynamic Logics, in Handbook of Philosophical Logics, Vol II, Gabbay-Guenthner, eds., Reidel 1984.
Hoare, C.A.R., Communicating Sequential Processes, Prentice Hall, 1985.
Hennessy, M., Milner, R., Algebraic Laws for Nondeterminism and Concurrency, Journal of ACM 32 1985.
Milner, R., A Calculus of Communicating Systems, LNCS 92, 1980.
Milner, R., Communication and Concurrency, Prentice Hall, 1989.
Mac Lane, S., Categories for the Working Mathematician, Springer-Verlag 1971.
Montanari, U., Sassone, V., Dynamic Disimulation, Technical Report TR-13/90, Dipartimento di Informatica, Univ. Pisa, 1990.
Manca, V., Salibra, A., Scollo, G., Equational Type Logic, Theoretical Computer Science, 77, 1990.
Montanari, U., Yankelevich, D., An Algebraic View of Interleaving and Distributed Operational Semantics, in Proc. Third Symposium on Category Theory and Computer Science, LNCS 389, 1989.
Park, D., Concurrency and Automata on Infinite Sequences, in Proc. GI, LNCS 104, 1981.
Nielsen, M., Plotkin, G. Winskel, G. Petri Nets, Event Structures and Domains. Theoretical Computer Science, 13, 1981.
Olderog, E.-R., Operational Petri Nets Semantics for CCSP, in Advances in Petri Nets 87, LNCS 266, 1987.
Pratt, V., Modelling Concurrency with Partial Orders, Int. Journal of Parallel Programming, 15, 1986.
Rabinovich, A. Trakhtenbrot, B. Behaviour Structures and Nets, Fundamenta Informaticae XI, 1988.
Reisig, W. Petri Nets: An Introduction, EATCS Monograph, Springer, 1985.
van Glabbeek, R. The Approximation Induction Principle in Process Alagebras, Proc. STACS'87, LNCS 397, 1987.
van Glabbeek, R., Goltz, U., Equivalence Notions for Concurrent Systems and Refinement of Actions, Proc. MFCS '89, LNCS 397, 1989.
Wand, M., Final Algebras Semantics and Data Type Extension, Journal of Comp. and System Science, 19, 1979.
Winskel, G., Event Structures Semantics for CCS and Related Languages, in Proc. ICALP 82, LNCS 140, 1982.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ferrari, GL., Montanari, U., Mowbray, M. (1991). On causality observed incrementally, finally. In: Abramsky, S., Maibaum, T.S.E. (eds) TAPSOFT '91. CAAP 1991. Lecture Notes in Computer Science, vol 493. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53982-4_2
Download citation
DOI: https://doi.org/10.1007/3-540-53982-4_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53982-7
Online ISBN: 978-3-540-46563-8
eBook Packages: Springer Book Archive