組成劃分為最小化是一種有效的減少狀态空間爆炸問題的技術。這種技術考慮幾個過程的并行組合。在其最簡單的形式中，每個順序流程都被一個抽象代替，比相應的流程更簡單，同時仍然保留所檢查的屬性。然而，這種技術不能應用于并行組合首先轉換為非确定性連續單片處理的環境。這個整體過程的優點是，它有助于對全局行為進行靜态分析。是以，我們提出了一種技術，該技術将一個帶有資料的整體流程視為一個整體流程，并将其分解為兩個流程，其中每個流程為整體流程的一個參數子集定義行為。我們證明了這些過程在合适的同步環境下保持了整體過程的特性。此外，我們證明了狀态不變量可以用來提高算法的有效性。最後，我們将分解技術應用于幾個規範。
原文：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.
Decompositional Minimisation of Monolithic Processes.pdf