基于模态逻辑D公理系统的Conformant规划方法  

Conformant Planning as Modal Logic Axiomatic System D

作　　者：吕帅[1,2] 刘磊[1,2] 李莹[1,2] 石莲[1,2] 

机构地区：[1]吉林大学计算机科学与技术学院,长春130012 [2]吉林大学符号计算与知识工程教育部重点实验室,长春130012

出　　处：《计算机研究与发展》2009年第7期1160-1168,共9页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(60603031;60773097;60873044);高等学校博士学科点基金项目(20050183065;20060183044;20070183057)~~

摘　　要：2006年,conformant规划问题成为国际规划竞赛不确定性问题域中的标准测试问题,得到研究人员的广泛关注.目前,conformant规划系统都是将其看成信念状态空间上的启发式搜索问题予以求解.通过分析conformant规划问题的语法和语义,提出新的基于模态逻辑的规划框架,将其转换为模态逻辑D公理系统的一系列定理证明问题.提出2种基于模态逻辑的编码方式,构造相应的公理与推理规则形成模态公式集,保证对于D系统的定理证明过程等同于原问题的规划过程,并通过问题实例验证该方法的有效性.继基于SAT、CSP、线性规划、模型检测等求解技术的规划方法后,该规划框架是基于转换的规划方法的一种新的尝试.More researchers have paid attention to conformant planning since conformant planning problems became the benchmarks of the undeterministic track of the International Planning Competition in 2006. Nowadays, all the planners which can be used to deal with conformant planning problems find a valid plan via searching the belief states in belief state spaces, which could be expressed as implicit structures or explicit formulas. In this paper, a novel modal logic-based planning framework is proposed by analyzing the grammars and modal semantics of the conformant problem definition. A conformant planning problem is translated into a series of automated reasoning problems based on the modal logic axiomatic system D. Based on this framework, two modal logic-based encodings and corresponding modal formulae sets are proposed by constructing the axioms and inference rules of the corresponding axiomatic systems, such as explanatory frame axioms, action necessity rules, etc. It ensures that the theorem proving processing of corresponding theorems in axiomatic system D is equivalent to the planning processing of the original problem. The soundness of this translation method is also illustrated. This method can be viewed as a novel attempt following the well known translation methods, which translate the original problems into SAT, CSP, linear programming, model checking, and so on.

关 键 词：conformant规划 模态逻辑 自动推理 可满足性 公理系统 D公理 

分 类 号：TP181[自动化与计算机技术—控制理论与控制工程]