An Executable Specification of Asynchronous Pi-Calculus Semantics and May Testing in Maude 2.0
Prasanna Thati, Koushik Sen, Narciso Martı́-Oliet · Electronic Notes in Theoretical Computer Science · 2004
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.