整体过程的分解极小化
Decompositional Minimisation of Monolithic Processes
摘要：
组合最小化可以是一种有效的技术，以减少状态空间爆炸问题。该技术考虑了多个进程的并行组合。在其最简单的形式中，每个顺序过程都被一个抽象所取代，这个抽象比相应的过程更简单，同时仍然保留了被检查的属性。然而，这种技术不能应用于并行组合首先转换为非确定性顺序单片过程的设置中。这种整体过程的优点是它便于对全局行为进行静态分析。因此，我们提出了一种技术，认为一个整体的过程中的数据和分解成两个过程，每个过程中定义的行为的一个子集的参数的整体过程。我们证明，这些进程保持一个合适的同步上下文中的单片进程的属性。此外，我们证明了状态不变量可以用来提高其有效性。最后，我们将分解技术应用到几个规格。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
