A Data Symmetry Reduction Technique for Temporal-epistemic Logic
A Data Symmetry Reduction Technique for Temporal-epistemic Logic
复制标题
时间认知逻辑的数据对称性降低技术
DOI：
10.1007/978-3-642-04761-9_6
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Hongyang Qu
中科院分区：
文献类型：
--
作者：
Mika Cohen;M. Dam;A. Lomuscio;Hongyang Qu
提出了一种用于时间认知逻辑模型检验的数据对称约简方法。该技术抽象的知识运营商的认识不可否认的关系，并保持时间认识公式。我们展示了一种静态检测数据对称性的方法，在ISPL程序中，输入到时间认知模型检查器MCMAS。我们报告的实验表明，在验证时间和空间的指数节省，同时验证的NSPK协议的安全属性。
We present a data symmetry reduction approach for model checking temporal-epistemic logic. The technique abstracts the epistemic indistinguishably relation for the knowledge operators, and is shown to preserve temporal-epistemic formulae. We show a method for statically detecting data symmetry in an ISPL program, the input to the temporal-epistemic model checker MCMAS. The experiments we report show an exponential saving in verification time and space while verifying security properties of the NSPK protocol.
结合故障注入和模型检查来验证多代理系统中的容错能力
DOI：
--
发表时间：
2009
期刊：
8th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS09)
影响因子：
--
作者：
Jonathan E
通讯作者：
Jonathan E