Abstract
For sequential programming, the theory of functions provides a uniform metalanguage to describe behaviours by abstracting from the actual implementation of programs. For concurrent and distributed systems, instead, there is no well accepted metalanguage to describe the possible observations of the behaviour of programs. The proper treatment of observations is thus an important and complex issue of concurrency theory. In this paper we show that observations can be described in a uniform way by introducing certain algebras called observation algebras. They lift to an algebraic level the standard treatment of actions in the operational semantics of process algebras. Observations are described as terms of an algebra. As a consequence, we separate the control level (the operational semantics) from the data level (the observations). The chosen notion of observability can be obtained by suitably axiomatizing the operations of the observation algebra. We show how observation algebras can be naturally derived from process algebras. As a case study we consider Milner's CCS. We introduce an observation algebra for CCS and we show that the standard interleaving semantics can be obtained by axiomatizing the operations to yield actions. Furthermore, we give a complete axiomatization of an observation algebra whose elements are certain labelled partial orderings of events (pomsets) called Spatial Pomsets.
Work partially supported by ESPRIT Basic Research Action 3011, CEDISYS, and by Progetto Finalizzato Informatica e Calcolo Parallelo, obiettivo LAMBRUSCO.
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
Austry, D. Boudol, G. Algebra de Processus et Synchronization, Theoretical Computer Science 30 (1), pp 91–131, 1984.
Boudol, G., Castellani, I., Concurrency and Atomicity, Theoretical Computer Science 59 (1,2), pp. 25–84, 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, pp 411–437 1989.
Boudol, G., Castellani, I., Three Equivalent Semantics Semantics for CCS, In Semantics of Systems of Concurrent Processes, LNCS 469, pp 96–141, 1990.
Boudol, G., Castellani, I., Kiehn, A., Hennessy, M., Observing Localities, To appear Proc. MFCS 1991, LNCS, 1991.
Brookes, S.D., Hoare, C.A.R., Roscoe, A.D., A Theory of Communicating Sequential Processes, Journal of ACM 31 (3), pp 560–599, 1984.
Bergstra, J., Klop, W., Process Algebra for Synchronous Communication, Information and Control 60, pp 109–137, 1984.
Clarke, E., Emerson, A., Sistla, P. Automatic Verifications of Finite State Concurrent Systems using Temporal Logic Specifications, ACM, TOPLAS, 8, pp 244–263, 1986.
Corradini, A., Ferrari, G., Montanari, U. Transition Systems with Algebraic Structure as Models of Computations, In Semantics of Systems of Concurrent Processes, LNCS 469, pp 185–222, 1990.
Degano, P., Montanari, U., Concurrent Histories: A Basis for Observing Distributed Systems, Journal of Computer and System Sciences 34, pp 422–461, 1987.
De Simone, R., Higher Level Synchronising Devices in MEIJE-SCCS, Theoretical Computer Science, 37 (3), pp 245–267, 1985.
Ferrari, G., Gorrieri, R., Montanari, U., An Extended Expansion Theorem, In Proc. TAPSOFT 91, LNCS 494, pp 29–48, 1991.
Ferrari, G., Montanari, U., Towards the Unification of Models for Concurrency, Proc. CAAP'90, LNCS 431, pp 162–176, 1990.
Harel, D. Dynamic Logic, In Handbook of Philosophical Logic, Vol II, (Gabbay-Guenthner Eds.), pp 497–604, 1984.
Hoare, C.A.R., Communicating Sequential Processes, Prentice Hall, 1985.
Hennessy, M. An Algebraic Theory of Processes, MIT Press, 1988.
Hennessy, M., Milner, R., Algebraic Laws for Nondeterminism and Concurrency, Journal of ACM 32 (1), pp 137–141, 1985.
Lamport, L. What Good is Temporal Logic, IFIP-83, pp 657–668, 1983.
Mazurkiewicz, A. Concurrent Program Schemes and their Interpretations, Technical Report DAIMI PB-78, Aarhus University, 1977.
Mazurkiewicz, A. Basic Notions of Trace Theory,In Proc. REX School, Workshop on Linear Time Branching Time and Partial Orders in Logics and Models for Concurrency, LNCS 354, pp 285–363, 1989.
Milner, R., A Calculus of Communicating Systems, LNCS 92, 1980.
Milner, R. A Modal Characterization of the Observable Machine Behaviour, In Proc. CAAP 81, LNCS 112, pp 25–34, 1981.
Milner, R., Communication and Concurrency, Prentice Hall, 1989.
Manna, Z., Pnueli, A. The Anchored Version of the Temporal Framework, In Proc. REX School, Workshop on Linear Time Branching Time and Partial Orders in Logics and Models for Concurrency, LNCS 354, pp 201–284 1989.
Park, D., Concurrency and Automata on Infinite Sequences, in Proc. GI, LNCS 104, pp 167–183, 1981.
Nielsen, M., Plotkin, G., Winskel, G. Petri Nets, Event Structures and Domains (Part I). Theoretical Computer Science, 13 (1), pp 85–108, 1981.
Plotkin, G. A Structured Approach to Operational Semantics, DAIMI FN-19, Computer Science Dept. University of Aarhus, 1981.
Plotkin, G., Pratt, W., Teams Can See Pomsets, Preliminary Report, August 1990.
Pratt, V., Modelling Concurrency with Partial Orders, Int. Journal of Parallel Programming, 15 (1), pp 381–400, 1986.
Reisig, W. Petri Nets: An Introduction, EATCS Monograph, Springer, 1985.
Stirling, C. Modal and Temporal Logics, To appear in Handbook of Logic in Computer Science, Vol I, (Gabbay-Maibaum Eds.) Oxford University Press.
Winskel, G. Event Structure Semantics for CCS and Related Languages, Proc. ICALP 82, LNCS 140, pp 561–576, 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, G.L., Montanari, U. (1991). The observation algebra of spatial pomsets. In: Baeten, J.C.M., Groote, J.F. (eds) CONCUR '91. CONCUR 1991. Lecture Notes in Computer Science, vol 527. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54430-5_89
Download citation
DOI: https://doi.org/10.1007/3-540-54430-5_89
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54430-2
Online ISBN: 978-3-540-38357-4
eBook Packages: Springer Book Archive