A well known technique to reduce the impact of the state space explosion problem problem is compositional minimisation. In this technique, first the state spaces of all components are computed and minimised modulo some behavioural equivalence (e.g., some form of bisimilarity). These minimised transition systems are subsequently combined to obtain the final state space.

In earlier work (by Maurice and Tim) a compositional minimisation technique was presented tailored to mCRL2: it provides support for the multi-action semantics of mCRL2 and allows splitting up a monolithic linear process specification into components. Only strong bisimulation minimisation of components could be used, limiting the effectiveness of the approach. In this talk I will present an extension to support branching bisimulation reduction. Additionally, I will present a number of benchmarks using mCRL2 models derived from railway SysML models, showing that a significant reduction can be achieved, also compared to compositional minimisation with strong bisimulation reduction.