A Comprehensive History of $μ$CRL and mCRL2
Logic in Computer Science
Summary
The authors describe the history and development of μCRL and its successor mCRL2, which are mathematical languages used to model and analyze how computer systems interact by sending messages. These formalisms are based on process algebra and other mathematical tools, making them both simple and expressive. The authors emphasize that mCRL2 is useful not only for theoretical work but also for practical tools that help understand complex systems. Their work focuses on ensuring that the communication in these systems is designed correctly by relying on strong mathematical foundations.
Authors
Jan Friso Groote, Erik P. de Vink
Abstract
This article gives a historical overview of the background, motivation and development of μCRL and its successor mCRL2, from the inception to the present. Both mCRL2 and μCRL are similar, compact, but very expressive formalisms based on process algebra, term rewriting, and the modal mu-calculus. They are developed to model and analyse the behaviour of interacting systems, i.e., systems that communicate by exchange of messages, among each other and with the outside world. Every contemporary computer system can be viewed as such an interacting system and their communication schemes are difficult to design correctly. By sticking to the mathematical foundations, but being led by the desire to be practically relevant, the formalism has grown to become very versatile. In particular, mCRL2 does not only foster the development of theory and the formulation of correctness proofs, but it is also the basis of a large set of automatic tools that help to provide insight in the behaviour of complex computer controlled systems.