ISR 2026 — 15th International School on Rewriting

Advanced Track lecturers: Rick Erkens and Jan Friso Groote

Model checking with the mCRL2 toolset: trillions of term rewriting steps. How to get it fast?

The mCRL2 language and toolset are used to model and analyse behaviour of communicating systems. mCRL2 uses process algebra, equational data types and the modal μ-calculus. It has not only be used for communication protocols and distributed systems, but also to completely describe and analyse embedded controllers, including the main controller of the Maeslantbarrier, which is the largest movable object in the world. The state spaces of such systems are huge, easily far larger than 10⁹ states.

At the core of mCRL2 are equational abstract data types. Term rewriting is the essential technique to evaluate data. For every state typically hundreds of terms must be rewritten. The basic question is how to take care that such Herculean rewriting tasks are executed in decent time. For this there are several techniques such as Just In Time Rewriting, the use of a compiling rewriter, several kinds of pattern matching automata and transducers.

The equational data types in mCRL2 are for good reasons slightly different from standard rewriting systems. A data type can have constructors, mappings and equations, and especially constructors are not exactly what you think. There is the possibility of using higher order functions. On top of this, standard data types have been defined, including numbers (with 64-bit digits), lists, sets and bag. Of course the datatypes reflect their mathematical counter part. Numbers are unlimited, and the set of all prime numbers can easily be denoted. But if they are not performant, they are of little use to analyse behavioral models.

Schedule

• Sunday 12 July, 09:00: A primer on mCRL2 and its use to model and analyse systems
• Sunday 12 July, 11:00: Semantics of mCRL2 data types. Standard rewriting rules for numbers and sets; Enumeration of summation operators and quantifiers.
• Monday 13 July, 13:30: Just in time rewriting. The compiling rewriter
• Monday 13 July, 15:30: Automaton-based algorithms for supporting fast term rewriting

Literature

1. www.mcrl2.org (the mcrl2 toolset can be downloaded here)
2. J.F. Groote and M.R. Mousavi. Modeling and analysis of communicating systems. The MIT press. 2014.
3. R. Erkens. Automaton-based techniques for optimized term rewriting (PhD thesis, Eindhoven University of Technology). 2024.