论文标题
基于培养皿的符号模型检查计算树知识的逻辑
Petri Net Based Symbolic Model Checking for Computation Tree Logic of Knowledge
论文作者
论文摘要
计算树知识的逻辑（CTLK）可以指定多代理系统（MAS）隐私和安全性的许多设计要求。在我们的会议论文中，我们定义了面向知识的培养皿（KPN），以建模MAS和具有等效关系（RGER）的拟议可及性图以验证CTLK。在本文中，我们使用有序的二进制决策图（OBDD）的技术编码rger，以减轻状态爆炸问题并提高验证效率。我们提出了一种启发式方法来订购OBDD中的这些变量，可以很好地改善生产，编码和探索巨大状态空间的时间和空间性能。更重要的是，我们的方法在产生和编码rger时不会产生和编码状态的任何过渡或等价关系，实际上，它会动态地产生CTLK公式验证过程中所需的过渡或等价关系。由于国家的过渡或等价关系的数量远大于州本身的数量，因此该策略可以节省大量时间和空间。我们设计符号模型检查算法，开发一个工具并将其应用于两个著名的示例：爱丽丝 - 鲍勃协议和餐饮密码师协议。我们将工具与MCMA进行比较，MCMA是验证CTLK的最新模型检查器。实验结果说明了我们的模型和方法的优势。我们在通用PC中运行的工具可以完全花费不到14个小时，以使用1200个并发密码学家验证餐饮密码器协议，其中约有$ 10^{1080} $状态，并且两个经过验证的CTLK公式具有6000多个原子命题，并有更多的3600多个操作员。这些良好的表现归功于OBDD技术和KPN的结构特征的组合。
Computation Tree Logic of Knowledge (CTLK) can specify many design requirements of privacy and security of multi-agent systems (MAS). In our conference paper, we defined Knowledge-oriented Petri Nets (KPN) to model MAS and proposed Reachability Graphs with Equivalence Relations (RGER) to verify CTLK. In this paper, we use the technique of Ordered Binary Decision Diagrams (OBDD) to encode RGER in order to alleviate the state explosion problem and enhance the verification efficiency. We propose a heuristic method to order those variables in OBDD, which can well improve the time and space performance of producing, encoding and exploring a huge state space. More importantly, our method does not produce and encode any transition or equivalence relation of states when producing and encoding an RGER, and in fact it dynamically produces those transition or equivalence relations that are required in the verification process of CTLK formulas. This policy can save a lot of time and space since the number of transition or equivalence relations of states is much greater than the number of states themselves. We design symbolic model checking algorithms, develop a tool and apply them to two famous examples: Alice-Bob Protocol and Dining Cryptographers Protocol. We compare our tool with MCMAS which is the state-of-the-art model checker of verifying CTLK. The experimental results illustrate the advantages of our model and method. Our tool running in a general PC can totally spend less than 14 hours to verify Dining Cryptographers Protocol with 1200 concurrent cryptographers where there are about $10^{1080}$ states and the two verified CTLK formulas have more than 6000 atomic propositions and more than 3600 operators. These good performances are owed to a combination of the OBDD technique and the structure characteristics of KPN.
