A Loop Acceleration Technique to Speed Up Verification of Automatically-Generated Plans

The CIRCA planning system automatically creates reactive plans and uses formal verification techniques to prove that those plans will preserve system safety.CIRCA’s timed au- tomata verification system is highly efficient, yet can dis- play pathologically bad behavior when reasoning about re- action loops , a particular form of interacting cycles of states. In this paper we describe a loop acceleration technique that recognizes these state space structures during the verification process and bypasses the process of expanding an arbitrarily large cycle of states, effectively compressing any size loop into a compact, finite set of states. The resulting performance improvement can be very dramatic: in domains where tight loops of short-duration transitions interact with long-duration transitions, our new loop acceleration methods can reduce verification time (and hence planning time) from hours to be- low a second.

Robert P. Goldman, Michael J.S. Pelican and David J. Musliner, "A Loop Acceleration Technique to Speed Up Verification of Automatically-Generated Plans", ICAPS workshop on Verification and Validation of Planning and Scheduling Systems, 2011. - [PDF]