An executable specification of asynchronous pi-calculus semantics and may testing in Maude 2.0. (English) Zbl 1272.68322
Gadducci, Fabio (ed.) et al., WRLA 2002. Proceedings of the 4th international workshop on rewriting logic and its applications, Pisa, Italy, September 19–21, 2002. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 71, 261-281 (2004).
Summary: We describe an executable specification of the operational semantics of an asynchronous version of the \(\pi\)-calculus in Maude by means of conditional rewrite rules with rewrites in the conditions. We also present an executable specification of the may testing equivalence on non-recursive asynchronous \(\pi\)-calculus processes, using the Maude metalevel. Specifically, we describe our use of the metaSearch operation to both calculate the set of all finite traces of a non-recursive process, and to compare the trace sets of two processes according to a preorder relation that characterizes may testing in asynchronous \(\pi\)-calculus. Thus, in both the specification of the operational semantics and the may testing, we make heavy use of new features introduced in version 2.0 of the Maude language and system.
For the entire collection see [Zbl 1271.68038].
For the entire collection see [Zbl 1271.68038].
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 68Q55 | Semantics in the theory of computing |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
References:
| [1] | Agha, G.: Actors: A model of concurrent computation in distributed systems. (1986) |
| [2] | Agha, G.: Concurrent object-oriented programming. Communications of the ACM 33, No. 9, 125-141 (September 1990) |
| [3] | Boreale, M.; De Nicola, R.: Testing equivalence for mobile processes. Information and computation 120, 279-303 (1995) · Zbl 0835.68073 |
| [4] | Boreale, M.; De Nicola, R.; Pugliese, R.: Proof techniques for cryptographic processes. Proceedings 14th IEEE symposium on logic in computer science, LICS’99, Trento, Italy, July 2-5, 1999, 157-166 (1999) · Zbl 1017.68050 |
| [5] | Boreale, M.; De Nicola, R.; Pugliese, R.: Trace and testing equivalence on asynchronous processes. Information and computation 172, No. 2, 139-164 (2002) · Zbl 1009.68079 |
| [6] | Borovanský, P.; Kirchner, C.; Kirchner, H.; Moreau, P. -E.; Vittek, M.: ELAN: A logical framework based on computational systems. Proceedings first international workshop on rewriting logic and its applications, WRLA’96, asilomar, California, September 3-6, 1996, volume 4 of electronic notes in theoretical computer science, 35-50 (1996) · Zbl 0912.68091 |
| [7] | Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Quesada, J. F.: Towards maude 2.0. Proceedings third international workshop on rewriting logic and its applications, WRLA 2000, Kanazawa, Japan, September 18-20, 2000, volume 36 of electronic notes in theoretical computer science, 297-318 (2000) · Zbl 0962.68108 |
| [8] | Mason, I. A.; Talcott, C.: A semantically sound actor translation. Automata, languages and programming, 24th international colloquium, ICALP’97, Bologna, Italy, July 7-11, 1997, Proceedings, volume 1256 of lecture notes in computer science, 369-378 (1997) · Zbl 1401.68026 |
| [9] | Merro, M.; Kleist, J.; Nestmann, U.: Local \({\pi}\)-calculus at work: mobile objects as mobile processes. Theoretical computer science: exploring new frontiers of theoretical informatics, international conference IFIP TCS 2000 Sendai, Japan, August 17-19, 2000, Proceedings, volume 1872 of lecture notes in computer science, 390-408 (2000) · Zbl 0998.68517 |
| [10] | Merro, M.; Sangiorgi, D.: On asynchrony in name-passing calculi. Automata, languages and programming, 25th international colloquium, ICALP’98, Aalborg, Denmark, July 13-17, 1998, Proceedings, volume 1443 of lecture notes in computer science, 856-867 (1998) · Zbl 0910.03019 |
| [11] | Milner, R.; Parrow, J.; Walker, D.: A calculus of mobile processes (Parts I and II). Information and computation 100, 1-77 (1992) · Zbl 0752.68037 |
| [12] | De Nicola, R.; Hennessy, M.: Testing equivalence for processes. Theoretical computer science 34, 83-133 (1984) · Zbl 0985.68518 |
| [13] | Plotkin, G. D.: A structural approach to operational semantics. (September 1981) |
| [14] | Stehr, M. -O.: CINNI – A generic calculus of explicit substitutions and its application to \({\lambda}, {\sigma}\) and \({\pi}\)-calculi. Proceedings third international workshop on rewriting logic and its applications, WRLA 2000, Kanazawa, Japan, September 18-20, 2000, volume 36 of electronic notes in theoretical computer science, 71-92 (2000) · Zbl 0966.68147 |
| [15] | Talcott, C.: An actor rewriting theory. Proceedings first international workshop on rewriting logic and its applications, WRLA ’96, asilomar, California, September 3-6, 1996, volume 4 of electronic notes in theoretical computer science, 360-383 (1996) · Zbl 0912.68086 |
| [16] | Thati, P.; Ziaei, R.; Agha, G.: A theory of May testing for actors. Proceedings IFIP TC6/WG6.1 fifth international conference on formal methods for open object-based distributed systems (FMOODS 2002), March 20-22, 2002, Enschede, The Netherlands, 147-162 (2002) · Zbl 1048.68059 |
| [17] | Thati, P.; Ziaei, R.; Agha, G.: A theory of May testing for asynchronous calculi with locality and no name matching. Algebraic methodology and software technology, 9th international conference, AM AST 2002, saint- gilles-LES-bains, Reunion Island, France, September 9-13, 2002, Proceedings, volume 2422 of lecture notes in computer science, 223-238 (2002) · Zbl 1275.68106 |
| [18] | Verdejo, A.; Martí-Oliet, N.: Implementing CCS in maude 2. Proceedings fourth international workshop on rewriting logic and its applications, WRLA 2002, Pisa, Italy, September 19-21, 2002, volume 71 of electronic notes in theoretical computer science, 239-257 (2002) |
| [19] | Viry, P.: Input/output for ELAN. Proceedings first international workshop on rewriting logic and its applications, WRLA’96, asilomar, California, September 3-6, 1996, volume 4 of electronic notes in theoretical computer science, 51-64 (1996) · Zbl 0912.68093 |
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.
