Abstract
We explore the implications of improvements in hardware and knowledge representation for the application of automated reasoning systems to planning. We apply a novel automated-reasoning system with no planningspecific features to questions about the PDDL planning domains Blocksworld and (no airports) Logistics. Our system, with no human interaction and considering no specific problem instances, is able to verify all the key state invariants for both domains. We propose organizing domain reasoning around (currently hand-written) recursive state-predicate– achievement macro-actions, such as a macro to achieve clear(b) in the Blocksworld. Leveraging (somewhat) limited human interaction, our system can completely characterize the effects of executing such recursive macros for each predicate in each domain. In addition, with substantial human interaction, our system can formally verify the solvability of arbitrary Blocksworld and Logistics problems, verifying a human-written generalized plan based on the macros. In each case, no specific problem instances are considered. We loosely meter and qualitatively characterize the human interaction required for the above verifications in order to stimulate research to reduce this benchmark until it is zero. We propose (and where possible estimate the benchmark improvement for) plausible future approaches to reducing interaction, including eliminating the need for hand-definitions of the recursive predicateachievement macros and generalized plans in these domains. Finally, we contrast our reasoning system favorably (for this task) with a widely used verification system, Coq.
Date of this Version
10-2-2013