Symmetry reduction in CSP model checking
Symmetry reduction in CSP model checking
复制标题
CSP 模型检查中的对称性降低
DOI：
10.1007/s10009-019-00516-4
复制
发表时间：
2019
影响因子：
1.5
通讯作者：
Gibson-Robinson T
中科院分区：
文献类型：
--
作者：
Gibson-Robinson T
我们提出了一个扩展的FDR，模型检查的进程代数CSP，利用对称性，以减少搜索的状态空间的大小。我们定义了一个过程相对于转换标签上的一组排列对称意味着什么。我们的因素的搜索对称等价的状态空间，映射每个状态的一个代表其等价类，从而考虑所有对称状态在一起。我们证明了一个强大的句法结果，识别条件下，一个过程将是对称的，在一个特定的类型。我们将展示如何实现这样一个搜索使用功能强大的技术的supercombinator的实现FDR：我们确定条件的supercombinator是对称的，并解释如何应用置换的状态。最后，我们提出了一种新的有效的技术来计算代表的等价类，通常会发现独特的代表;我们的实验表明，这种技术通常比其他技术工作得更快，特别是规模更好。
We present an extension of FDR, the model checker for the process algebra CSP, that exploits symmetry to reduce the size of the state space searched. We define what it means for a process to be symmetric with respect to a group of permutations on the transition labels. We factor the state space of the search by symmetry equivalence, mapping each state to a representative of its equivalence class, thereby considering all symmetric states together. We prove a powerful syntactic result, identifying conditions under which a process will be symmetric in a particular type. We show how to implement such a search using the powerful technique of supercombinators used in the implementation of FDR: we identify conditions on a supercombinator for it to be symmetric and explain how to apply a permutation to a state. Finally, we present a novel efficient technique for calculating representatives of equivalence classes, which normally finds unique representatives; our experiments suggest that this technique typically works faster than other techniques and in particular scales better.
登录
查看更多内容
用于面向属性的模型检查的看门狗转换
DOI：
--
发表时间：
2003
期刊：
FME
影响因子：
--
作者：
M. Goldsmith;N. Moffat;B. Roscoe;Tim Whitworth;Irfan Zakiuddin
通讯作者：
Irfan Zakiuddin
无名稿号（将由编辑插入） 通过对称标记对 B 和 Z 模型进行高效近似验证
DOI：
--
发表时间：
--
期刊：
影响因子：
--
作者：
A. Lanot;A. Boyer;T. Lobbedez;C. Béchade
通讯作者：
C. Béchade
使用 CSP 分析无锁线性化数据类型
DOI：
--
发表时间：
2017
期刊：
Concurrency, Security, and Puzzles
影响因子：
--
作者：
G. Lowe
通讯作者：
G. Lowe
FDR3：CSP 的并行细化检查器
DOI：
10.1007/s10009-015-0377-y
发表时间：
2015
影响因子：
1.5
作者：
Gibson-Robinson T
通讯作者：
Gibson-Robinson T
用于 CSP 细化检查的对称性利用的代表性函数方法
DOI：
--
发表时间：
2008
期刊：
IEEE International Conference on Formal Engineering Methods
影响因子：
--
作者：
N. Moffat;M. Goldsmith;B. Roscoe
通讯作者：
B. Roscoe