Abstract
We explore the features of rewriting logic and the 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 previously, it cannot be directly executed in the 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 the 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. This executable specification plus the reflective control of the rewriting process can be used to analyze CCS processes.
The original version of this chapter was revised: The copyright line was incorrect. This has been corrected. The Erratum to this chapter is available at DOI: 10.1007/978-0-387-35533-7_26
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Bruni. Tile Logic for Synchronized Rewriting of Concurrent Systems. PhD thesis, Dipartimento di Informatica, Università di Pisa, 1999.
M. Clavel. Reflection in General Logics and in Rewriting Logic with Applications to the Maude Language. PhD thesis, University of Navarre, 1998.
M. Clavel, F. Duran, S. Eker, P. Lincoln, N. Marti-Oliet, J. Meseguer, and J. Quesada. Maude: Specification and Programming in Rewriting Logic. SRI International, Jan. 1999, revised Aug. 1999.
M. Clavel, F. Duran, S. Eker, P. Lincoln, N. Marti-Oliet, J. Meseguer, and J. Quesada. Using Maude. In Proc. FASE 2000, LNCS 1783. Springer, 2000.
R. Cleaveland, J. Parrow, and B. Steffen. The Concurrency Workbench: A semantics-based tool for the verification of finite-state systems. ACM Transactions on Programming Languages and Systems, 15 (1): 36–72, Jan. 1993.
M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32 (1): 137–161, Jan. 1985.
N. Marti-Oliet and J. Meseguer. Rewriting logic as a logical and semantic framework. Technical Report SRI-CSL-93–05, SRI International, 1993. To appear in Handbook of Philosophical Logic, Kluwer Academic Publishers.
J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96: 73–155, 1992.
R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
J. Quemada, editor. Final committee draft on Enhancements to LOTOS. ISO/IEC JTC1/SC21/WG7 Project 1.21.20.2.3., May 1998.
M.-O. Stehr and J. Meseguer. Pure type systems in rewriting logic. In Proc. of LFM’99: Workshop on Logical Frameworks and Meta-Languages, France, 1999.
C. Stirling. Modal and temporal logics for processes. In Logics for Concurrency: Structure vs Automata, LNCS 1043, pages 149–237. Springer, 1996.
A. Verdejo and N. Marti-Oliet. Executing and verifying CCS in Maude. Technical Report 99–00, Dpto. Sistemas Informâticos y Programación, Universidad Complutense de Madrid, Feb. 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Verdejo, A., Martí-Oliet, N. (2000). Implementing CCS in Maude. In: Bolognesi, T., Latella, D. (eds) Formal Methods for Distributed System Development. PSTV FORTE 2000 2000. IFIP — The International Federation for Information Processing, vol 55. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35533-7_22
Download citation
DOI: https://doi.org/10.1007/978-0-387-35533-7_22
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5264-9
Online ISBN: 978-0-387-35533-7
eBook Packages: Springer Book Archive