The Formal Specification Language mCRL2

Authors Jan Friso Groote, Aad Mathijssen, Michel Reniers, Yaroslav Usenko, Muck van Weerdenburg

Thumbnail PDF


  • Filesize: 410 kB
  • 34 pages

Document Identifiers

Author Details

Jan Friso Groote
Aad Mathijssen
Michel Reniers
Yaroslav Usenko
Muck van Weerdenburg

Cite AsGet BibTex

Jan Friso Groote, Aad Mathijssen, Michel Reniers, Yaroslav Usenko, and Muck van Weerdenburg. The Formal Specification Language mCRL2. In Methods for Modelling Software Systems (MMOSS). Dagstuhl Seminar Proceedings, Volume 6351, pp. 1-34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)


We introduce mCRL2, a specification language that can be used to specify and analyse the behaviour of distributed systems. This language is the successor of the mCRL specification language. The mCRL2 language extends a timed basic process algebra with the possibility to define and use abstract data types. The mCRL2 data language features predefined and higher-order data types. The process algebraic part of mCRL2 allows a faithful translation of coloured Petri nets and component based systems: we have introduced multiactions and we have separated communication and parallelism.
  • Specification language
  • abstract data types
  • process algebra
  • operational semantics


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail