Open Systems Laboratory at Illinois

An executable specification of asynchronous pi-calculus semantics and may testing in maude 2.0

By Prasanna Thati, Koushik Sen, and Narciso Martí-Oliet. Electr. Notes Theor. Comput. Sci, 71:261–281, 2002.

Full Text:
Download PDF
Publisher Link:


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.


    author = "Thati, Prasanna and Sen, Koushik and Martí-Oliet,
    title = "An Executable Specification of Asynchronous Pi-Calculus
             Semantics and May Testing in Maude 2.0",
    ee = "",
    journal = "Electr. Notes Theor. Comput. Sci",
    keywords = "formal methods",
    pages = "261-281",
    volume = "71",
    year = "2002",