A static view of localities
Tóm tắt
This paper proposes alternative, effective characterizations for nets of automata of the location equivalence and preorder presented by Boudol et al. in the companion paper [BCHK]. Contrary to the technical development in the above given reference, where locations are dynamically associated to the subparts of a process in the operational semantics, the equivalence and preorder we propose are based on a static association of locations to the parallel components of a net. Following this static approach, it is possible to give these “distributed nets” a standard operational semantics which associates with each net a finite labelled transition system. Using this operational semantics for distributed nets, we introduce effective notions of equivalence and preorder which are shown to coincide with those proposed in [BCHK].
Tài liệu tham khảo
Aceto, L.: A static view of localities. Rapport de Recherche 1483, INRIA, Sophia Antipolis, Valbonne, July 1991.
Boudol, G. and Castellani, I.: A non-interleaving semantics for CCS based on proved transitions.Fundamenta Informaticae, 11(4):433–452, 1988.
Boudol, G., Castellani, I., Hennessy, M. and Kiehn, A.: A theory of processes with localities. This volume.
Boudol, G., Castellani, I., Hennessy, M. and Kiehn, A.: Observing localities. Technical Report 4/91, University of Sussex, March 1991. To appear inTheoretical Computer Science. An extended abstract appeared in theProceedings of MFCS '91, LNCS 520.
Castellani, I.:Bisimulations for concurrency, PhD thesis, Report CST-51-88, Department of Computer Science, University of Edinburgh, April 1988.
Castellani, I. and Hennessy, M.: Distributed bisimulations.Journal of the ACM, 36(4):887–911, 1989.
Darondeau, P. and Degano, P.: Causal trees. Publication Interne No. 442, IRISA, Rennes Cedex, France, 1988. An extended abstract appeared in: Proceedings ICALP 89, Stresa (G. Ausiello, M. Dezani-Ciancaglini & S. Ronchi Della Rocca), LNCS 372, Springer-Verlag, pp. 234–248.
Degano, P., De Nicola, R. and Montanari, U.: Universal axioms for bisimulation, 1992. To appear inTheoretical Computer Science.
Degano, P. and Priami, C: Proved trees. In Kuich [Kui92], pages 629–640.
Fernandez, J.-C.: Aldébaran: a tool for verification of communicating processes. Technical report SPECTRE cl4, LGI-IMAG, Grenoble, 1989.
Inverardi, P., Priami, C. and Yankelevich, D.: Verification of concurrent systems in SML, June 1992. To appear inProceedings of the ACM Sigplan Workshop on ML and its applications, San Francisco.
Kiehn, A.: Distributed bisimulations for finite CCS. Technical Report 7/89, University of Sussex, 1989.
Kiehn, A.: Local and global causes. Technical Report 342/23/91, Technische Universitat Munchen, 1991.
Krishnan, P.: Distributed CCS. In J.C.M. Baeten and J.F. Groote, editors,Proceedings CONCUR 91, Amsterdam, volume 527 ofLecture Notes in Computer Science, pages 393–407. Springer-Verlag, 1991.
Kuich, W.: editor.Proceedings 19 th ICALP, Vienna, volume 623 ofLecture Notes in Computer Science. Springer-Verlag, 1992.
Larsen, K.G.: Efficient local correctness checking (extended abstract), 1992. Accepted for CAV '92.
Milner, R.:Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, 1989.
Malhotra, J., Smolka, S., Giacalone, A. and Shapiro, R.: Winston, a tool for hierarchical design and simulation of concurrent systems. InWorkshop on Specification and Verification of Concurrent Systems, Stirling, Scotland, 1988.
Montanari, U. and Yankelevich, D.: A parametric approach to localities. In Kuich [Kui92], pages 617–628.
de Simone, R. and Vergamini, D.: Aboard AUTO. Technical Report 111, INRIA, Centre Sophia-Antipolis, Valbonne Cedex, 1989.
Yankelevich, D.: Inducing preorders on observation trees. Technical Memo HP-PSC-92-33, Hewlett-Packard, Pisa Science Center, April 1992.