mCRL is a language for specifying and verifying distributed systems
in an algebraic fashion. It targets the specification of system
behaviour in a process-algebraic style and of data elements in the
form of abstract data types. The mCRL toolset supports the analysis
and manipulation of mCRL specifications. A mCRL specification can be
automatically transformed into a linear process operator (LPO). All
other tools in the mCRL toolset use LPOs as their starting point.
The simulator allows the interactive simulation of an LPO. There are
a number of tools that allow optimisations on the level of LPOs. The
instantiator generates a labelled transition system from an LPO,
which can be visualised, analysed and minimised.
