RT Journal Article
T1 Executing and verifying CCS in Maude
A1 Verdejo López, José Alberto
A1 Martí Oliet, Narciso
AB 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.
YR 2000
FD 2000-02
LK https://hdl.handle.net/20.500.14352/57576
UL https://hdl.handle.net/20.500.14352/57576
LA spa
DS Docta Complutense
RD 8 may 2024