Implementing CCS in Maude 2 Export

@article{citeulike:3501463, 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.}, author = {Verdejo, A. and Martioliet, N.}, citeulike-article-id = {3501463}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/S1571-0661(05)82540-X}, citeulike-linkout-1 = {http://linkinghub.elsevier.com/retrieve/pii/S157106610582540X}, doi = {10.1016/S1571-0661(05)82540-X}, issn = {15710661}, journal = {Electronic Notes in Theoretical Computer Science}, keywords = {concurrency, maude}, month = {April}, pages = {282--300}, posted-at = {2008-11-10 16:38:50}, priority = {0}, title = {Implementing CCS in Maude 2}, url = {http://dx.doi.org/10.1016/S1571-0661(05)82540-X}, volume = {71}, year = {2004} }

TY - JOUR ID - citeulike:3501463 L3 - citeulike-article-id:3501463 N2 - 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. JF - Electronic Notes in Theoretical Computer Science SN - 15710661 EP - 300 TI - Implementing CCS in Maude 2 VL - 71 SP - 282 KW - concurrency KW - maude AU - Verdejo, A AU - Martioliet, N PY - 2004/04// UR - http://dx.doi.org/10.1016/S1571-0661(05)82540-X ER -