基于谨慎语义的规划证明系统

Proof Systems for Planning Under Cautious Semantics

近年来关于不完全知识的规划成为活跃的研究领域,许多逻辑系统引入感知动作、条件规划描述这一问题。作为代表性的成果之一,Son和Baral提出了动作语言Ak及其不完全信息下的推理语义。本研究进一步为Ak设计了谨慎语义和弱谨慎语义,使得主体可以在严格安全环境下生成并执行可靠的规划。计算复杂性分析表明谨慎语义降低了Ak的推理复杂性;为上述语义提出用于验证条件规划推理机制的Hoare型证明系统,该系统是可靠和完全的,既可应用于规划生成,又可应用于规划验证;且该系统有离线规划的性质,即在离线状态下主体可以将已有的短的证明组成新的长的证明。

Planning with incomplete knowledge becomes a very active research area recently.Many logical formalisms introduce sensing actions and conditional plans to address the problem.The action language Ak invented by Son and Baral is a well-known framework for this purpose.In this paper,we propose so-called cautious and weakly cautious semantics for Ak,in order to allow an agent to generate and execute reliable plans in safety-critical environment.Intuitively speaking,cautious and weakly cautious semantics enable the agent to know exactly what happens after the execution of an action.Computational complexity analysis shows that cautious semantics reduces the reasoning complexity of Ak.Another important contribution of our work is the development of Hoare style proof systems.These proof systems are served as inference mechanisms for the verification of conditional plans,and proved to be sound and complete.In addition,they could be used for plan generation,in the sense that constructing a derivation is indeed the procedure to finding a plan.The proof systems possess a property for off-line planning,the agent could generate and store short proofs in her spare time,then perform quick plan query by easily constructing a long proof from the stored shorter ones.