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

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

本项目将描述逻辑的能力和特征引入到对行动的刻画和推理中，结合模型检测途径，构建基于描述逻辑和模型检测的行动理论及应用平台，为行动理论的发展和应用提供新的途径。具体来说，本项目研究了命题动态逻辑的描述逻辑扩展，构建了一簇扩展的动态描述逻辑DDL(X@)，给出了有效的Tableau判定算法和推理机制。研究了基于动态描述逻辑的知识表示和推理问题，构建了基于动态描述逻辑的行动理论。构建了基于通信系统演算和描述逻辑的复杂行动表示系统，可以在动态描述逻辑的基础上对并行、同步、通信、中断、以及无终止地执行等控制结构进行刻画。研究了时序描述逻辑ALC-LTL的可满足性问题，给出了有效的Tableau判定算法和推理机制。将动态描述逻辑与时序描述逻辑结合起来，构建了具有可判定性的分支时序动态描述逻辑和线性时序动态描述逻辑，给出了相应的Tableau判定算法和推理机制。研究了时序描述逻辑的模型检测问题，将描述逻辑的推理机制与时序逻辑的模型检测机制结合起来，给出了时序描述逻辑的模型检测算法。研究了基于符号技术的描述逻辑推理机制和模型检测算法，开发了相应的软件原型系统。最后，研究了上述逻辑系统及推理机制在语义Web服务发现、组合和验证，以及在智能诊断、几何公差类型生成、访问控制、装配序列规划等领域的应用。