×

zbMATH — the first resource for mathematics

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:
Linda
PDF BibTeX XML Cite
Full Text: DOI
References:
[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 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, (), 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, (), 95-109
[9] Boreale, M.; De Nicola, R.; Pugliese, R., A theory of “may” testing for asynchronous languages, (), 165-179
[10] Boreale, M.; Fournet, C.; Laneve, C., Bisimulations in the join calculus, () · 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, (), 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 New York, p. 372-385
[18] Fournet, C.; Gonthier, G., A hierarchy of equivalences for asynchronous calculi, (), 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 Cambridge · Zbl 0437.68002
[22] Honda, K.; Tokoro, M., An object calculus for asynchronous communication, (), 133-147
[23] Honda, K.; Tokoro, M., On asynchronous communication semantics, (), 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 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 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)
[31] Montanari, U.; Pistore, M., Finite state verification for the asynchronous π-calculus, (), 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 Los Alamitos, p. 46-57
[33] Pugliese, R., A process calculus with asynchronous communications, (), 295-310
[34] Rathke, J., Resource based models for asynchrony, (), 273-287
[35] Selinger, P., First-order axioms for asynchrony, (), 376-390
[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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.