Guiding planner backjumping using verifier traces

In this paper, we show how a planner can use a model-checking verifier to guide state space search. In our work on hard real-time, closed-loop planning, we use a model-checker’s reachability computations to determine whether plans will be successfully executed. For planning to pro-ceed efficiently, we must be able to efficiently repair can-didate 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 manufac-turing scheduling