Advertisement

On causality observed incrementally, finally

  • Gian-Luigi Ferrari
  • Ugo Montanari
  • Miranda Mowbray
CAAP Colloquium On Trees In Algebra And Programming
Part of the Lecture Notes in Computer Science book series (LNCS, volume 493)

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.

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

  1. [Ab 88]
    Abramsky, S., A Domain Equation for Bisimulation, Internal report, Dept. Computing, Imperial CollegeGoogle Scholar
  2. [AD 89]
    Arnold, A., Dicky, A., An Algebraic Characterization of Transition System Equivalences, Information and Computation 82, 1989.Google Scholar
  3. [BC 88]
    Boudol, G., Castellani, I., Concurrency and Atomicity, Theoretical Computer Science 59, 1988.Google Scholar
  4. [BC 89]
    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.Google Scholar
  5. [BK 84]
    Bergstra, J., Klop, W., Process Algebra for Synchronous Communication, Information and Control 60, 1984.Google Scholar
  6. [DD 89]
    Darondeau, P., Degano, P. Causal Trees, In Proc. ICALP 89, LNCS 372, 1989.Google Scholar
  7. [DDM 87]
    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.Google Scholar
  8. [DDM 88a]
    Degano, P. De Nicola, R., Montanari, U. A Distributed Operational Semantics for CCS Based on Condition/Event Systems. Acta Informatica, 26, 1988.Google Scholar
  9. [DDM 88b]
    Degano, P. De Nicola, R., Montanari, U. On the Consistency of Truly Concurrent Operational and Denotational Semantics. Proc. LICS 1988.Google Scholar
  10. [DDM 89]
    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.Google Scholar
  11. [DDM 90]
    Degano, P. De Nicola, R., Montanari, U. A Partial Ordering Semantics for CCS, Theoretical Computer Science 75, 1990.Google Scholar
  12. [DMM 89]
    Degano, P., Meseguer, J., Montanari, U., Axiomatizing Net Computations and Processes, in Proc. Logics in Computer Science 89, 1989.Google Scholar
  13. [DM 87]
    Degano, P., Montanari, U., Concurrent Histories: A Basis for Observing Distributed Systems, Journal of Computer and System Sciences 34, 1987.Google Scholar
  14. [DF 90]
    De Nicola, R. Ferrari, G. Observational Logics and Concurrency Models, Proc 10th Conf. FST and TCS, LNCS 472, 1990Google Scholar
  15. [Fe 90]
    Ferrari, G. Unifying Models of Concurrency, PhD Thesis, TD/4-90, Dipartimento di Informatica, Univ. Pisa, 1990.Google Scholar
  16. [FM 90]
    Ferrari, G., Montanari, U., Towards the Unification of Models for Concurrency, Proc. CAAP'90, LNCS 431, 1990.Google Scholar
  17. [Go 88]
    Goltz, U. On Representing CCS Programs by Finite Petri Nets, Proc. MFCS 88, LNCS 324, 1988.Google Scholar
  18. [Gog 72]
    Goguen, J. Realization is Universal, Math. Systems Theory, 6, 1972.Google Scholar
  19. [GGM 76]
    Giarratana, V., Gimona, F., Montanari, U. Observability Concepts in Abstract Data Type Specifications, in Proc. MFCS 76, LNCS 45, 1976.Google Scholar
  20. [GM 90]
    Gorrieri, R., Montanari, U., SCONE: a Simple Calculus of Nets, In Proc. CONCUR'90, LNCS 458, 1990.Google Scholar
  21. [GR 83]
    Goltz, U., Reisig, W., The Non Sequential Behaviour of Petri Nets, Information and Computation 57, 1983.Google Scholar
  22. [Ha 84]
    Harel, D. Dynamic Logics, in Handbook of Philosophical Logics, Vol II, Gabbay-Guenthner, eds., Reidel 1984.Google Scholar
  23. [Ho 85]
    Hoare, C.A.R., Communicating Sequential Processes, Prentice Hall, 1985.Google Scholar
  24. [HM 85]
    Hennessy, M., Milner, R., Algebraic Laws for Nondeterminism and Concurrency, Journal of ACM 32 1985.Google Scholar
  25. [Mil 80]
    Milner, R., A Calculus of Communicating Systems, LNCS 92, 1980.Google Scholar
  26. [Mil 89]
    Milner, R., Communication and Concurrency, Prentice Hall, 1989.Google Scholar
  27. [ML 71]
    Mac Lane, S., Categories for the Working Mathematician, Springer-Verlag 1971.Google Scholar
  28. [MS 90]
    Montanari, U., Sassone, V., Dynamic Disimulation, Technical Report TR-13/90, Dipartimento di Informatica, Univ. Pisa, 1990.Google Scholar
  29. [MSS 90]
    Manca, V., Salibra, A., Scollo, G., Equational Type Logic, Theoretical Computer Science, 77, 1990.Google Scholar
  30. [MY 89]
    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.Google Scholar
  31. [Pa 81]
    Park, D., Concurrency and Automata on Infinite Sequences, in Proc. GI, LNCS 104, 1981.Google Scholar
  32. [NPW 81]
    Nielsen, M., Plotkin, G. Winskel, G. Petri Nets, Event Structures and Domains. Theoretical Computer Science, 13, 1981.Google Scholar
  33. [Ol 87]
    Olderog, E.-R., Operational Petri Nets Semantics for CCSP, in Advances in Petri Nets 87, LNCS 266, 1987.Google Scholar
  34. [Pr 86]
    Pratt, V., Modelling Concurrency with Partial Orders, Int. Journal of Parallel Programming, 15, 1986.Google Scholar
  35. [RT 88]
    Rabinovich, A. Trakhtenbrot, B. Behaviour Structures and Nets, Fundamenta Informaticae XI, 1988.Google Scholar
  36. [Re 85]
    Reisig, W. Petri Nets: An Introduction, EATCS Monograph, Springer, 1985.Google Scholar
  37. [vG 87]
    van Glabbeek, R. The Approximation Induction Principle in Process Alagebras, Proc. STACS'87, LNCS 397, 1987.Google Scholar
  38. [vGG 89]
    van Glabbeek, R., Goltz, U., Equivalence Notions for Concurrent Systems and Refinement of Actions, Proc. MFCS '89, LNCS 397, 1989.Google Scholar
  39. [Wa 79]
    Wand, M., Final Algebras Semantics and Data Type Extension, Journal of Comp. and System Science, 19, 1979.Google Scholar
  40. [Win 82]
    Winskel, G., Event Structures Semantics for CCS and Related Languages, in Proc. ICALP 82, LNCS 140, 1982.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • Gian-Luigi Ferrari
    • 1
  • Ugo Montanari
    • 2
  • Miranda Mowbray
    • 3
  1. 1.IEI CNRPisaItaly
  2. 2.Dipartimento di InformaticaUniversità di PisaPisaItaly
  3. 3.Hewlett-Packard Science CentrePisaItaly

Personalised recommendations