Push-1 is PSPACE-complete, and the automated verification of motion planning gadgets

Abstract

Push-1 is one of the simplest abstract frameworks for motion planning; however, the complexity of deciding if a Push-1 problem can be solved was a several-decade-old open question. We resolve the complexity of the motion planning problem Push-1 by showing that it is PSPACE-complete, and we formally verify the correctness of our constructions. Our results build upon a recent work which demonstrated that Push-1F (a variant of Push-1 with fixed blocks) and Push-k for $k \geq 2$ (a variant of Push-1 where the agent can push $k$ blocks at once) are PSPACE-complete and more generally on the motion-planning-though-gadgets framework. In the process of resolving this open problem, we make two general contributions to the motion planning complexity theory. First, our proof technique extends the standard motion planning framework by assigning the agent a state. This state is preserved when traversing between gadgets but can change when taking transitions in gadgets. Second, we designed and implemented a system, GADGETEER, for computationally verifying the behavior of systems of gadgets. This system is agnostic to the underlying motion planning problem, and allows for formally verifying the correspondence between a low-level construction and a high-level system of gadgets as well as automatically synthesizing gadgets from low-level constructions. In the case of Push-1, we use this system to formally prove that our constructions match our high-level specifications of their behavior. This culminates in the construction and verification of a self-closing door, as deciding reachability in a system of self-closing doors is PSPACE-complete.