Guiding Planner Backjumping Using Verifier Traces

All Papers

In this paper, we show how a planner can use a modelchecking verifier to guide state space search. In our work on hard real-time, closed-loop planning, we use a modelchecker’s reachability computations to determine whether plans will be successfully executed. For planning to proceed efficiently, we must be able to efficiently repair candidate plans that are not correct. Reachability verifiers can return counterexample traces when a candidate plan violates desired properties. A core contribution of our work is our technique for automatically extracting repair candidates from counterexample traces. We map counterexample traces onto a search algorithm’s choice stack to direct backjumping. We prove that our technique will not sacrifice completeness, and present empirical results showing substantial performance improvements in difficult cases. Our results can be applied to other applications, such as automatic design, and manufacturing scheduling.