局部状态空间分析辅助部分降阶
Local State Space Analysis to Assist Partial Order Reduction
摘要：
本文提出了一种更有效的模型检验并发系统的偏序约简方法。该方法利用组合可达性分析为并发系统中的所有进程生成过近似的局部状态转换模型，其中可以提取独立关系和其他有用的信息。提取的独立关系，相比可以通过静态分析系统描述，更精确和细化，因此导致更有效的偏序约简。这种方法是证明了一组并发系统的例子。与使用SPIN可以获得的相比，在几种情况下已经观察到状态空间的显著更高的减少。
英文摘要：
This paper presents an approach to more efficient partial order reduction for model checking concurrent systems. This approach utilizes a compositional reachability analysis to generate over-approximate local state transition models for all processes in a concurrent system where an independence relation and other useful information can be extracted. The extracted independence relation, compared to what can be obtained by statically analyzing the system descriptions, is more precise and refined, therefore leads to more efficient partial order reduction. This approach is demonstrated on a set of concurrent system examples. Significantly higher reduction in state space has been observed in several cases compared to what can be obtained using SPIN.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
