多智体系统时序认知规范的SPIN模型检测

Multi-Agent System SPIN Model Checking Based on the Temporal Logic of Knowledge

SPIN模型检测器主要用来检测线性时序逻辑描述的规范,而多智体系统的规范采用时序认知逻辑描述比较方便。本文着重讨论了如何利用SPIN模型检测线性时序认知逻辑的方法,根据局部命题的理论,将模型检测知识算子和公共算子表述的规范规约为模型检测线性时序逻辑的问题,从而使SPIN的检测功能由线性时序逻辑扩充到线性时序认知逻辑。本文通过一个RPC协议分析实例来说明模型检测线性时序认知逻辑的方法。

A SPIN model checker is mainly used to check whether a system satisfies the specifications expressed in linear temporal logic,and the specifications of the distributed systems and protocols expressed in knowledge logic are more convenient.In this paper,the model checking approaches for the temporal logic of knowledge using SPIN are discussed.According to the theory of partial proposition,the problem of how to model check knowledge operators and public knowledge operators is converted into model checking linear temporal logic.These approaches make SPIN＇s functions extended from model checking temporal logic to the linear temporal logic of knowledge.The article discusses the approach of model checking the linear temporal logic of knowledge by analyzing an instance of the RPC protocol.