μCRL和mCRL2的全面历史
A Comprehensive History of $μ$CRL and mCRL2
浏览论文内容
中文总结 AI 辅助
本文回顾μCRL及其后续mCRL2的发展历程，它们基于进程代数等用于交互系统建模分析。该形式化方法兼顾数学基础与实用性，mCRL2推动理论发展，还是众多自动工具基础，助力理解复杂计算机控制系统行为。
中文摘要 AI 辅助
本文对μCRL及其后续版本mCRL2从起源到现在的背景、动机和发展进行了历史概述。mCRL2和μCRL都是基于进程代数、项重写和模态μ-演算的相似、紧凑但表达力很强的形式化方法。它们用于对交互系统行为建模和分析。当代计算机系统可视为交互系统，其通信方案难设计正确。该形式化方法坚持数学基础且注重实用性，变得非常通用。特别是mCRL2不仅促进理论发展和正确性证明表述，还是大量自动工具的基础，有助于洞察复杂计算机控制系统行为。
英文摘要
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.
