A monolithic process is a single recursive equation with data parameters, which only uses non-determinism, action prefixing, and recursion. We present a technique that decomposes such a monolithic process into multiple processes where each process defines behaviour for a subset of the parameters of the monolithic process. For this decomposition we can show that a composition of these processes is strongly bisimilar to the monolithic process under a suitable synchronisation context. Minimising the resulting processes before determining their composition can be used to derive a state space that is smaller than the one obtained by a monolithic exploration. We apply the decomposition technique to several specifications to show that this works in practice. Finally, we prove that state invariants can be used to further improve the effectiveness of this decomposition technique.

翻译：单石化过程是一个单一的递归方程式, 包含数据参数, 仅使用非确定性、 动作前置和递归。 我们展示了一种技术, 将这种单石化过程分解成多个过程, 每个过程为单石化过程的一组参数界定行为。 对于这种分解, 我们可以证明这些过程的构成在适当的同步环境下与单石化过程非常相似。 在确定其组成之前, 最小化所产生的过程可用于获取比单石化勘探所获得的小的空间。 我们将解腐化技术应用于几个规格, 以表明这种工艺在实际中是有效的。 最后, 我们证明, 可以使用状态变异物来进一步提高这种分解技术的有效性 。