Executing and Verifying CCS in Maude

Alberto Verdejo and Narciso Martí-Oliet

We explore the features of rewriting logic and, in particular, of the rewriting logic lan- guage Maude as a logical and semantic framework for representing and executing inference systems. In order to illustrate the general ideas, we have represented both the seman- tics of Milner's CCS and a modal logic for describing local capabilities of CCS processes. Although a rewriting logic representation of the CCS semantics was given previously, it cannot be directly executed in the current default interpreter of Maude. Moreover, it cannot be used to answer questions such as which are the successors of a process after performing an action, which is used to de ne the semantics of Hennessy-Milner modal logic. Basically, the problems are the existence of new variables in the righthand side of the rewrite rules and the nondeterministic application of the semantic rules, inherent to CCS. We show how these problems can be solved in a general, not CCS dependent way by exploiting the re ective properties of rewriting logic, which allow controlling the rewriting process. We also show how the semantics can be extended to traces of actions and to the CCS weak transition relation. This executable speci cation plus the re ective control of the rewriting process can be used to analyze CCS processes.

(BibTeX entry)    (gzip'ed Postscript)   


back   home   Formal Methods and Declarative Languages Laboratory   Computer Science Laboratory, SRI International