Computational complexity of reasoning about plans

Abstract: "The artificial intelligence (AI) planning problem is known to be very hard in the general case. Propositional planning is PSPACE-complete and first-order planning is undecidable. Many planning researchers claim that all this expressiveness is needed to solve real problems and some of them have abandoned theory-based planning methods in favour of seemingly more efficient methods. These methods usually lack a theoretical foundation so not much is known about the correctness and the computational complexity of these. There are, however, many applications where both provable correctness and efficiency are of major concern, for instance, within automatic control. We suggest in this thesis that it might be possible to stay within a well-founded theoretical framework and still solve many interesting problems tractably. This should be done by identifying restrictions on the planning problem that improve the complexity figure while still allowing for interesting problems to be modelled. Finding such restrictions may be a non-trivial task, though. As a first attempt at finding such restrictions we present a variant of the traditional STRIPS formalism, the SAS[superscript +] formalism. The SAS[superscript +] formalism has made it possible to identify certain restrictions which define a computationally tractable planning problem, the SAS[superscript +]-PUS problem, and which would not have been easily identified using the traditional STRIPS formalism. We also present a polynomial-time, sound and complete algorithm for the SAS[superscript +]-PUS problem. We further prove that the SAS[superscript +] formalism in its unrestricted form is equally expressive as some other well-known formalisms for propositional planning. Hence, it is possible to compare the SAS[superscript +] formalism with these other formalisms and the complexity results carry over in both directions. Furthermore, we analyse the computational complexity of various subproblems lying between unrestricted SAS[superscript +] planning and the SAS[superscript +]-PUS problem. We find that most planning problems (not only in the SAS[superscript +] formalism) allow instances having exponentially-sized minimal solutions and we argue that such instances are not realistic in practice. We conclude the thesis with a brief investigation into the relationship between the temporal projection problem and the planning and plan validation problems."