Formalizing Goal Serializability for Evaluation of Planning Features.

Evaluation of the properties of various planning techniques such as completeness and termination plays an important role in choosing an appropriate planning technique for a particular planning problem. In this paper, we use the already existing formal specification of two well-known and classic state space planning techniques, forward state space planning and goal stack state space planning techniques, in Transaction Logic(T R) to study their completeness. Our study shows that using T R, we can formally specify the serializability of planning problems and prove the completeness of STRIPS planning problems for planning problems with serializable goals.