Trace and testing equivalence on asynchronous processes. (English) Zbl 1009.68079
Summary: We study trace and may-testing equivalences in the asynchronous versions of CCS and \(\pi\)-calculus. We start from the operational definition of the may-testing preorder and provide finitary and fully abstract trace-based characterizations for it, along with a complete in-equational proof system. We also touch upon two variants of this theory by first considering a more demanding equivalence notion (must-testing) and then a richer version of asynchronous CCS. The results throw light on the difference between synchronous and asynchronous communication and on the weaker testing power of asynchronous observations.
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 68M14 | Distributed systems |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
Software:
LindaReferences:
| [1] | Amadio, R. M.; Castellani, I.; Sangiorgi, D., On bisimulations for the asynchronous π-calculus, Theor. Comput. Sci., 195, 291-324 (1998) · Zbl 0915.68009 |
| [2] | Abadi, M.; Gordon, A. D., A calculus for cryptographic protocols: The spi calculus, Inform. and Comput., 148, 1-70 (1999) · Zbl 0924.68073 |
| [3] | Agha, G. A.; Mason, I. A.; Smith, S. F.; Talcott, C. L., A foundation for actor computation, J. Funct. Programming, 7, 1-72 (1997) · Zbl 0870.68091 |
| [4] | Bergstra, J.; Klop, J. W., Process algebra for synchronous communication, Inform. and Control, 60, 109-137 (1984) · Zbl 0597.68027 |
| [5] | de Boer, F. S.; Klop, J. W.; Palamidessi, C., Asynchronous communication in process algebra, Proc. of LICS’92 (1992), IEEE Comput. Soc: IEEE Comput. Soc Los Alamitos, p. 137-147 |
| [6] | de Boer, F. S.; Kok, J. N.; Palamidessi, C.; Rutten, J. J.M. M., The failure of failures in a paradigm for asynchronous communication, (Baeten, J. C.M.; Groote, J. F., Proc. of CONCUR’91 (1991), Springer-Verlag: Springer-Verlag Berlin), 111-126 |
| [7] | Boreale, M.; De Nicola, R., Testing equivalence for mobile systems, Inform. and Comput., 120, 279-303 (1995) · Zbl 0835.68073 |
| [8] | Boreale, M.; De Nicola, R.; Pugliese, R., Asynchronous observations of processes, (Nivat, M., Proc. of Foundations of Software Science and Computation Ssructures (FoSSaCS’98) (1998), Springer-Verlag: Springer-Verlag Berlin), 95-109 |
| [9] | Boreale, M.; De Nicola, R.; Pugliese, R., A theory of “May” testing for asynchronous languages, (Thomas, W., Proc. of Foundations of Software Science and Computation Ssructures (FoSSaCS’99) (1999), Springer-Verlag: Springer-Verlag Berlin), 165-179 |
| [10] | Boreale, M.; Fournet, C.; Laneve, C., Bisimulations in the join calculus, (Gries, D.; De Roever, W., Proc. of PROCOMET’98 (1998), Chapman & Hall: Chapman & Hall London) · Zbl 0989.68098 |
| [11] | Boudol, G., Asynchrony in the π-calculus (Note) (1992), INRIA Sophia-Antipolis |
| [12] | Busi, N.; Gorrieri, R.; Zavattaro, G.-L., A process algebraic view of Linda coordination primitives, Theor. Comput. Sci., 192, 167-199 (1998) · Zbl 0895.68016 |
| [13] | Castellani, I.; Hennesy, M., Testing theories for asynchronous languages, (Arvind, V.; Ramanujam, R., Proc. of FSTTCS (1998), Springer-Verlag: Springer-Verlag Berlin), 90-101 |
| [14] | De Nicola, R.; Hennessy, M. C.B., Testing equivalence for processes, Theor. Comput. Sci., 34, 83-133 (1984) · Zbl 0985.68518 |
| [15] | De Nicola, R.; Pugliese, R., Linda based applicative and imperative process algebras, Theor. Comput. Sci., 238, 389-437 (2000) · Zbl 0944.68064 |
| [16] | De Nicola, R.; Segala, R., A process algebraic view of I/O automata, Theor. Comput. Sci., 138, 391-423 (1995) · Zbl 0874.68209 |
| [17] | Fournet, C.; Gonthier, G., The reflexive chemical abstract machine and the join calculus, Proc. of the ACM Symp. on Principles of Programming Languages (1996), Assoc. Comput. Mach: Assoc. Comput. Mach New York, p. 372-385 |
| [18] | Fournet, C.; Gonthier, G., A hierarchy of equivalences for asynchronous calculi, (Larsen, k:G.; Skyum, S.; Winskel, G., Proc. of ICALP’98 (1998), Springer-Verlag: Springer-Verlag Berlin), 844-855 · Zbl 0909.03030 |
| [19] | Gelernter, D., Generative communication in Linda, ACM Trans. Programming Lang. Systems, 7, 80-112 (1985) · Zbl 0559.68030 |
| [20] | Hansen, M.; Huttel, H.; Kleist, J., Bisimulations for asynchronous mobile processes, Proc. of the Tiblisi Symposium on Language, Logic, and Computation (1995), University of EdimburghHuman Communication Research Centre |
| [21] | Hennessy, M. C.B., Algebraic Theory of Processes (1988), MIT Press: MIT Press Cambridge · Zbl 0437.68002 |
| [22] | Honda, K.; Tokoro, M., An object calculus for asynchronous communication, (America, P., Proc. of ECOOP’91 (1991), Springer-Verlag: Springer-Verlag Berlin), 133-147 |
| [23] | Honda, K.; Tokoro, M., On asynchronous communication semantics, (Tokoro, M.; Nierstratz, O.; Wegner, P., Object-Based Concurrent Computing (1991), Springer-Verlag: Springer-Verlag Berlin), 21-51 |
| [24] | Jonsson, B., A model and a proof system for asynchronous networks, Proc. of the 4th ACM Symposium on Principles of Distributed Computing (1985), Assoc. Comput. Mach: Assoc. Comput. Mach New York, p. 49-58 |
| [25] | Jifeng, H.; Josephs, M. B.; Hoare, C. A.R., A theory of synchrony and asynchrony, Proc. of the IFIP Working Conf. on Programming Concepts and Methods (1990), p. 446-465 |
| [26] | Lynch, N. A.; Stark, E. W., A proof of the Kahn principle for input/output automata, Inform. and Comput., 82, 81-92 (1989) · Zbl 0679.68119 |
| [27] | Lamport, L., The temporal logic of actions, ACM transactions on Programming Languages and Systems, 16, 872-923 (1994) |
| [28] | Milner, R., Communication and Concurrency (1989), Prentice-Hall: Prentice-Hall New York · Zbl 0683.68008 |
| [29] | Milner, R., The Polyadic π-calculus: A Tutorial (1991), University of Edinburgh |
| [30] | Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes (Part I and II), Inform. and Comput., 100, 1-77 (1992) · Zbl 0752.68037 |
| [31] | Montanari, U.; Pistore, M., Finite state verification for the asynchronous π-calculus, (Cleaveland, R., Proc. of TACAS’99 (1999), Springer-Verlag: Springer-Verlag Berlin), 255-269 |
| [32] | Pnueli, A., The temporal logic of programs, Proc. of the 18th IEEE Symposium on Foundations of Computer Science (1977), IEEE Comput. Soc: IEEE Comput. Soc Los Alamitos, p. 46-57 |
| [33] | Pugliese, R., A process calculus with asynchronous communications, (De Santis, A., Proc. of the 5th Italian Conference on Theoretical Computer Science (1995), World Scientific: World Scientific Singapore), 295-310 |
| [34] | Rathke, J., Resource based models for asynchrony, (Nivat, M., Proc. of Foundations of Software Science and Computation Ssructures (FoSSaCS’98) (1998), Springer-Verlag: Springer-Verlag Berlin), 273-287 |
| [35] | Selinger, P., First-order axioms for asynchrony, (Mazurkiewicz, A.; Winkowski, J., Proc. of CONCUR’97 (1997), Springer-Verlag: Springer-Verlag Berlin), 376-390 · Zbl 1512.68098 |
| [36] | Tretmans, J., A Formal Approach to Conformance Testing (1992), University of Twente |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
