Implementing CCS in Maude 2

Alberto Verdejo and Narciso Martí-Oliet

In F. Gadducci and U. Montanari, editors, Proceedings Fourth International Workshop on Rewriting Logic and its Applications, WRLA 2002, Pisa, Italy, September 19-21, 2002, volume 71 of Electronic Notes in Theoretical Computer Science, pages 239-257. Elsevier, 2002.

Abstract: 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.

  [pdf]

@InProceedings{VerdejoMarti-Oliet02,
  author =       {Alberto Verdejo and Narciso Mart{\'\i}-Oliet},
  title =        {Implementing {CCS} in {Maude} 2},
  crossref =     {GadducciMontanari02},
  pages =        {239-257},
  editor =       {Fabio Gadducci and Ugo Montanari},
  booktitle =    {Proceedings Fourth International Workshop on Rewriting
                  Logic and its Applications, WRLA 2002, Pisa, Italy,
                  September 19--21, 2002},
  year =         2002,
  publisher =    {Elsevier},
  volume =       71,
  series =       {Electronic Notes in Theoretical Computer Science},
  note =         {\url{http://www.elsevier.nl/locate/entcs/volume71.html}}
}