About

From MCRL2

mCRL2 stands for micro Common Representation Language 2. It is a specification language that can be used to specify and analyse the behaviour of distributed systems and protocols and is the successor to μCRL. Using its accompanying toolset systems can be analysed and verified automatically.

Philosophy

mCRL2 is based on the Algebra of Communicating Processes (ACP) which is extended to include data and time. Like in every process algebra, a fundamental concept in mCRL2 is the process. Processes can perform actions and can be composed to form new processes using algebraic operators. A system usually consists of several processes (or components) in parallel.

A process can carry data as its parameters. The state of a process is a specific combination of parameter values. This state may influence the possible actions that the process can perform. In turn, the execution of an action may result in a state change. Every process has a corresponding state space or Labeled Transition System (LTS) which contains all states that the process can reach, along with the possible transitions between those states.

Using the algebraic operators, very complex processes can be constructed containing, for example, lots of parallelism. A central notion in mCRL2 is the linear process. This is a process from which all parallelism has been removed to produce a series of condition - action - effect rules. Complex systems, consisting of hundreds or even thousands of processes, can be translated to a single linear process. Even for systems with an infinite state space, the linear process (being an abstract representation of that state space) is finite and can often be obtained very easily. Therefore, most tools in the mCRL2 toolset operate on linear processes rather than on state spaces.

Model checking is provided using Parameterised Boolean Equation Systems (PBES). Given a linear process and a formula that expresses some desired behaviour of the process, a PBES can be generated. The solution to this PBES indicates whether the formula holds on the process or not. An attempt can be made to remove data from a PBES in order to obtain a BES, which is often easier to solve.

Toolset

The mCRL2 toolset contains tools to automatically:

• Translate any mCRL2 specification to a linear process.
• Manipulate and simulate linear processes.
• Generate the state space associated with a linear process.
• Manipulate and visualize state spaces.
• Generate a PBES from a formula and a linear process.
• Generate a BES from a PBES.
• Manipulate and solve (P)BESs.

People

The following persons and many others have contributed to the toolset:

• Jan Friso Groote
• Jeroen Keiren
• Aad Mathijssen
• Bas Ploeger
• Frank Stappers
• Carst Tankink
• Yaroslav Usenko
• Muck van Weerdenburg
• Wieger Wesselink
• Jeroen van der Wulp