MCRL2

This article has multiple issues. Please help improve it or discuss these issues on the talk page. (Learn how and when to remove these messages) This article includes a list of general references, but it lacks sufficient corresponding inline citations. Please help to improve this article by introducing more precise citations. (April 2024) (Learn how and when to remove this message) This article includes a list of references, related reading, or external links, but its sources remain unclear because it lacks inline citations. Please help improve this article by introducing more precise citations. (April 2024) (Learn how and when to remove this message) (Learn how and when to remove this message)

mCRL2 is a specification language for describing concurrent discrete event systems. It is accompanied with a toolset, that facilitates tools, techniques and methods for simulation, analysis and visualization of behaviour. The behavioural part of the language is based on process algebra (Algebra of Communicating Processes). The data part of the toolset is based on abstract equational data types extended with higher-order functions.

The toolset was founded by Jan Friso Groote and is currently developed by the Formal Systems Analysis group at Eindhoven University of Technology, The Netherlands.