The mCRL2 Toolset for Analysing Concurrent Systems: Improvements in
Expressivity and Usability

Olav Bunte, Jan Friso Groote, Jeroen J.A. Keiren, Maurice Laveaux, Thomas Neele,
Erik P. de Vink, Wieger Wesselink, Anton Wijs andTim A.C. Willemse

Reasoning about the correctness of parallel and distributed systems
requires automated tools. By now, the mCRL2 toolset and language have
been developed over a course of more than fifteen years. In this
paper, we report on the progress and advancements over the past six
years. Firstly, the mCRL2 language has been extended to support the
modelling of probabilistic behaviour. Furthermore, the usability has
been improved with the addition of refinement checking, counterexample
generation and a user-friendly GUI. Finally, several performance
improvements have been made in the treatment of behavioural
equivalences. Besides the changes to the toolset itself, we cover
recent applications of mCRL2 in software product line engineering and
the use of domain specific languages (DSLs).