Implementing CCS in Maude 2

Alberto Verdejo and Narciso Martí-Oliet

This paper describes in detail how to bridge the gap between theory and practice in a new implementation of the CCS operational semantics in Maude, where transitions become rewrites and inference rules become conditional rewrite rules with rewrites in the conditions, as made possible by the new features in Maude 2.0. We implement both the usual transition semantics and the weak transition semantics where internal actions are not observed, and on top of them we also implement the Hennessy-Milner modal logic for describing processes. We compare this implementation with a previous one where transitions become judgements and inference rules become rewrites, and also comment on extensions to the LOTOS language.

(BibTeX entry)    (gzip'ed Postscript)   

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