In an mCRL2 specification the user can specify processes with data, that can in turn be manipulated through the computational model of term rewriting. The term rewriter that the toolset uses now is reasonably fast and yet the bottleneck for state space generation is often found in the rewriter. This calls for optimizing this part of the toolset. Unfortunately the term rewriter as it is implemented now, is not very comprehensible and hardly reflects the theoretical backbone of this model of computation.
In this talk I will give an introduction on the problems that we’ve encountered so far in our effort to rewrite the term rewriter. After this brief introduction we will discuss our latest efforts to obtain optimal matching algorithms for term rewrite systems through the use of match trees. This is still a work in progress.