Conformant Planning as Modal Logic Axiomatic System D

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.