A Symmetry Reduction Technique for Model Checking Temporal-Epistemic Logic
A Symmetry Reduction Technique for Model Checking Temporal-Epistemic Logic
复制标题
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Mika Cohen;Mads Dam;A. Lomuscio;Hongyang Qu
中科院分区：
文献类型：
--
作者：
Mika Cohen;Mads Dam;A. Lomuscio;Hongyang Qu
我们介绍了一个对称性约简技术的时间认知属性的多智能体系统的主流解释系统框架中定义的模型检查。该技术基于对应语义，旨在减少模型中需要考虑的初始状态集。我们提出的理论结果，建立既没有假阳性，也没有假阴性的简化模型。我们评估的技术，提出了两个著名的应用程序的认知逻辑，泥泞的孩子和用餐密码测试的实施结果。所获得的实验结果证实，模型检查时间的减少可以是戏剧性的，从而允许验证迄今棘手的系统。
We introduce a symmetry reduction technique for model checking temporal-epistemic properties of multi-agent systems defined in the mainstream interpreted systems framework. The technique, based on counterpart semantics, aims to reduce the set of initial states that need to be considered in a model. We present theoretical results establishing that there are neither false positives nor false negatives in the reduced model. We evaluate the technique by presenting the results of an implementation tested against two well known applications of epistemic logic, the muddy children and the dining cryptographers. The experimental results obtained confirm that the reduction in model checking time can be dramatic, thereby allowing for the verification of hitherto intractable systems.