Executing and verifying CCS in Maude

Abstract

We explore the features of rewriting logic and its language Maude as a logical and semantic framework for representing both the semantics of CCS, and a modal logic for describing local capabilities of CCS processes. Although a rewriting logic representation of the CCS semantics was given in [MOM93], 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 define 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 by exploiting the reflective 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 specification plus the reflective control of the rewriting process can be used to analyze CCS processes.