Observing located concurrency
We present a process algebra with an explicit notion of location, and give an operational semantics for it that distinguishes between processes with different distributions. We then introduce a denotational semantics parameterised by a topology over the set of locations; this topology allows observers to regard some locations as indistinguishable. We show that the denotational semantics is fully abstract if the topology satisfies the separation axiom T1, and that it coincides with the usual interleaving operational semantics if it is indiscrete, thus giving a criteria for when a given notion of 'indistinguishable location' corresponds to completely distributed or interleaved settings.
The algebra we consider is then extended to allow communication between different locations. A natural communication operator gives rise to a form of expansion theorem which allows us to extend full abstraction to this setting.
KeywordsTransition System Operational Semantic Parallel Composition Label Transition System Process Algebra
Unable to display preview. Download preview PDF.
- 1.L. Aceto, A static theory of localities, Technical Report Number 1483, Inria, 1991.Google Scholar
- 2.L. Aceto, Relating distributed, temporal and causal observations of simple processes, manuscript, HP Science Center Pisa, submitted for publication, 1992.Google Scholar
- 3.A. Arkhangel'skii and V. Ponomarev, Fundamentals of general topology, D. Reidel, 1984.Google Scholar
- 4.J. Baeten and W. Weijland, Process algebra, Cambridge Tracts in Theoretical Computer Science, Volume 18, Cambridge University Press, 1990.Google Scholar
- 5.G. Boudol, I. Castellani, M. Hennessy, and A. Kiehn, A theory of processes with locality, Technical Report 13/91, Department of Computer Science, University of Sussex, 1991.Google Scholar
- 6.I. Castellani and M. Hennessy, Distributed bisimulations, Journal of the ACM, Volume 10 (1989), Pp. 887–911.Google Scholar
- 7.A. Kiehn, Local and global causes, Technical Report 342/23/91 A, Institut für Informatik, Technische Universität München, 1991.Google Scholar
- 8.R. Milner, Communication and concurrency, International series on computer science, Prentice Hall International, 1989.Google Scholar
- 9.U. Montanari and D. Yankelevich, A Parametric Approach to Localities, in the Proceedings of ICALP '92, (W. Kuich, Ed.), Springer-Verlag LNCS, Volume 623.Google Scholar
- 10.D. Murphy, The physics of observation; a perspective for concurrency theorists, Bulletin of the EATCS, Volume 44 (1991), Pp. 192–200.Google Scholar
- 11.-, Intervals and actions in a timed process algebra, Arbeitspapiere der GMD 680, Gesellschaft für Mathematik und Dataverarbeitung, St. Augustin, 1992. Presented at MFPS '92 and submitted to Theoretical Computer Science.Google Scholar
- 12.D. Park, Concurrency and automata on infinite sequences, in Proceedings of Theoretical Computer Science 1981, Volume 104, Springer-Verlag LNCS, 1981.Google Scholar
- 13.G. Winskel, Synchronization trees, Theoretical Computer Science, Volume 34 (1985), Pp. 34–84.Google Scholar