| Abstract:Classic Planning has been one of the most important research topics in AI. However the complexity of solving planning problem has encumbered its application in real-life. As a result, analytical study delving into the complexity issue of planning has been a popular topic among researchers. We try to study the complexity of planning from a logic perspective. In this thesis we propose a novel approach, to describe planning with formal logic language, and furthermore we provide the corresponding algorithm to translate it into traditional action-based planning description. Up to our knowledge, before us, there is no existing method that is able to interpret general-descried PSPACE problem as action-based planning formalisms.Our approach is based on Second-order Logic with Transitive Closure (SO(TC)). To begin with, we propose a normal form for SO(TC) and prove its completeness, thereby obtaining a normalization algorithm for all formulae under its realm. In addition, we propose a reduction that directly translates this normal form into a planning problem to complete our approach. The resulting language encrypts a "domain+problem" combination using the versatile planning description language——PDDL. The value of our approach can be reflected in a few facets. On one hand, this method allows us to use planning technique to solve logic model checking problem which are either hand-coded or obtained by translating from other formal descriptions. On the other hand, the formal logic we use here can be seen as a compact and unified description of planning which we believe would be beneficial for analytical study.This algorithm is implemented with C++programming language, is able to generate PDDL-code that can be directly fed into planning problem solvers. In addition to that, we prove some important theoretical properties of our algorithm. One of which testifies that our approach, while translating problems into a PSPACE framework, is able to preserve the complexity class NP. |
PDF Full Text Request