多智体系统时态认知规范的模型检测算法

A Model Checking Algorithm for Temporal Logics of Knowledge in Multi-Agent Systems

模型检测技术一直以来主要是检验用时态逻辑描述的规范,人们很少注意认知逻辑的模型检测问题,而在分布式系统领域,系统和协议的规范已广泛地采用知识逻辑来描述.着重研讨了时态认知逻辑的模型检测算法.在SMV(symbolicmodelverifier)模型检测器的基础上,根据知识的语义和集合理论,提出了多种检验知识和公共知识的算法,从而使SMV的检测功能由时态逻辑扩充到时态认知逻辑.这些方法也适用于其他以状态集合作为输出的模型检测方法和工具的功能扩充.

Model checking has being used mainly to check if a system satisfies the specifications expressed in temporal logic and people pay little attention to the model checking problem for logics of knowledge. However, in the distributed systems community, the desirable specifications of systems and protocols have been expressed widely in logics of knowledge. In this paper, the model checking approaches for the temporal logic of knowledge are discussed. On the base of SMV (symbolic model verifier), according to the semantics of knowledge and set theory, several approaches for model checking of knowledge and common knowledge are presented. These approaches make SMV抯 functions extended from temporal logics to temporal logics of knowledge. They also correspond to other model checking approaches and tools where the output is the set of states.