基于描述逻辑和模型检测的行动理论研究

项目名称： 基于描述逻辑和模型检测的行动理论研究

项目编号： No.60903079

项目类型： 青年科学基金项目

立项/批准年度： 2010

项目学科： 金属学与金属工艺

项目作者： 常亮

作者单位： 桂林电子科技大学

项目金额： 18万元

中文摘要： 行动理论是知识表示和推理中重要的研究课题，是当前成为研究热点的语义Web服务和智能主体的理论基础。针对目前行动理论存在的局限，本项目将描述逻辑的能力和特征引入到对行动的刻画和推理中，结合模型检测途径，建立具有适用性和实用性的基于描述逻辑和模型检测的行动理论。首先，从命题动态逻辑的描述逻辑扩展出发，构建一簇与描述逻辑家族兼容的扩展的动态描述逻辑，填补当前行动理论之间存在的断层。在此基础上，引入通信系统演算CCS的刻画成分，构建基于CCS和描述逻辑的复杂行动表示系统，相应地提出扩展的模态mu演算及其模型检测方法，实现丰富的对复杂行动及其性质的刻画和验证。最后，将逻辑推理途径与模型检测途径结合起来，实现描述能力、推理或验证的性质、适用范围、以及计算复杂度等方面的互补，构建基于描述逻辑和模型检测的行动理论及应用平台，为行动理论的发展和应用提供新的途径。

中文关键词： 描述逻辑；行动理论；动态逻辑；模型检测；语义Web服务

英文摘要：

英文关键词： description logic；action theory；dynamic logic；model checking；semantic Web service