  Compositional minimisation can be an effective technique to reduce the state
space explosion problem. This technique considers a parallel composition of
several processes. In its simplest form, each sequential process is replaced by
an abstraction, simpler than the corresponding process while still preserving
the property that is checked. However, this technique cannot be applied in a
setting where parallel composition is first translated to a non-deterministic
sequential monolithic process. The advantage of this monolithic process is that
it facilitates static analysis of global behaviour. Therefore, we present a
technique that considers a monolithic process with data and decomposes it into
two processes where each process defines behaviour for a subset of the
parameters of the monolithic process. We prove that these processes preserve
the properties of the monolithic process under a suitable synchronisation
context. Moreover, we prove that state invariants can be used to improve its
effectiveness. Finally, we apply the decomposition technique to several
specifications.
