An Executable Specification of Asynchronous Pi-Calculus Semantics and May Testing in Maude 2.0

@article{citeulike:3500173, abstract = {We describe an executable specification of the operational semantics of an asynchronous version of the \&\#x3c0;-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 \&\#x3c0;-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 \&\#x3c0;-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.}, author = {Thati, P. and Sen, K. and Martioliet, N.}, citeulike-article-id = {3500173}, doi = {10.1016/S1571-0661(05)82539-3}, issn = {15710661}, journal = {Electronic Notes in Theoretical Computer Science}, keywords = {maude, picalculus}, month = {April}, pages = {261--281}, posted-at = {2008-11-10 07:05:46}, priority = {0}, title = {An Executable Specification of Asynchronous Pi-Calculus Semantics and May Testing in Maude 2.0}, url = {http://dx.doi.org/10.1016/S1571-0661(05)82539-3}, volume = {71}, year = {2004} }

TY - JOUR ID - citeulike:3500173 L3 - citeulike-article-id:3500173 N2 - We describe an executable specification of the operational semantics of an asynchronous version of the π-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 π-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 π-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. JF - Electronic Notes in Theoretical Computer Science SN - 15710661 EP - 281 TI - An Executable Specification of Asynchronous Pi-Calculus Semantics and May Testing in Maude 2.0 VL - 71 SP - 261 KW - maude KW - picalculus AU - Thati, P AU - Sen, K AU - Martioliet, N PY - 2004/04// UR - http://dx.doi.org/10.1016/S1571-0661(05)82539-3 ER -