A Representative Function Approach to Symmetry Exploitation for CSP Refinement Checking
A Representative Function Approach to Symmetry Exploitation for CSP Refinement Checking
复制标题
用于 CSP 细化检查的对称性利用的代表性函数方法
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
B. Roscoe
中科院分区：
文献类型：
--
作者：
N. Moffat;M. Goldsmith;B. Roscoe
存在有效的时序逻辑模型检查算法，其利用由多个相同组件的并行组合产生的对称性。这些算法通常采用一个函数rep从状态到代表状态下的对称性开发。我们适应这个想法的过程代数CSP的细化检查的上下文中。在这样做的时候，我们必须科普细化式的规范。然而，主要的挑战是需要获得足够的本地信息的状态，使一个有用的repfunction的定义，因为编译CSP过程的标签转换系统（LTS）呈现状态信息的全局属性，而不是一个本地的。使用结构化形式的实现过渡系统，我们获得了一个有效的对称性利用CSP细化检查算法，概括它在两个方向，并证明了所有三个变量的简单例子。
Effective temporal logic model checking algorithms exist that exploit symmetries arising from parallel composition of multiple identical components. These algorithms often employ a function repfrom states to representative states under the symmetries exploited. We adapt this idea to the context of refinement checking for the process algebra CSP. In so doing, we must cope with refinement-style specifications. The main challenge, though, is the need for access to sufficient local information about states to enable definition of a useful repfunction, since compilation of CSP processes to Labelled Transition Systems (LTSs) renders state information a global property instead of a local one. Using a structured form of implementation transition system, we obtain an efficient symmetry exploiting CSP refinement checking algorithm, generalise it in two directions, and demonstrate all three variants on simple examples.