AAAI Publications, Workshops at the Twenty-Sixth AAAI Conference on Artificial Intelligence

Font Size: 
Using Classical Planners for Plan Verification and Counterexample Generation
Robert P. Goldman, Ugur Kuter, Tony Schneider

Last modified: 2012-07-15


We are working to develop plan critiquing methods where a planner is used to identify flaws in an existing plan, in order to provide assistance to human planners. In this paper, we describe how to use any classical planning algorithm for verification and counterexample generation for plans already generated by some agent (human or an automated planning system). We show how to take an original classical planning domain, problem, and plan, and a set of uncontrollable (disturbance) actions and agents, and compile those inputs into a new "counter-planning'' problem. This counter-planning problem can be given to an arbitrary PDDL planner, in order to generate counterexample traces where uncontrollable actions can upset plan execution. Our experiments with a large set of planning problems in two multi-agent, dynamic planning domains demonstrated that our approach can verify a plan or generate a counterexample quickly and reliably. We have also compared our approach with a state-of-the-art model-checking system: the results suggest that using classical planners for generating counter plans is more promising than model-checking based verification.


planning; verification; critiquing

Full Text: PDF