Efficient Term Rewriting for mCRL2

Muck van Weerdenburg (OAS)

One of the bottlenecks in model checking is the time (and space) consuming transformation of a model to a state space. The main activity in such a transformation is often the rewriting of data expressions. In this talk I will give an overview of my work on the rewriter(s) of the mCRL2 toolset. This toolset differs from other such toolsets in that it has a higher order data specification language (amongst other features).