系统规范表示与验证的认识逻辑途径

本课题从分布式系统设计中的规范表示及其形式化验证的需要出发，研究多智能体的认识逻辑的模型检测技术。?围绕知识和信念的表示和建模，我们将提出新型实用的Kripke语义模型。我们也将考虑基于所提出的Kripke语义模型的知识融合和更新问题，并探讨它们与模型检测问题的关系。作为本课题的具体应用，拟开展基于认识逻辑的安全协议验证的模型检测方法研究。对于分布式系统（或多智能体系统），总体来说，还没有在规范表示与形式化验证两方面都令人满意的知识逻辑模型可以使用。本课题将试图通过有认识逻辑的基础理论和关键技术的研究，提出和实现新的知识逻辑模型及其相关算法，从而有可能在系统规范及其验证的研究方面取得实质性进展。