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

TL;DR

This paper proves that the simple motion planning problem Push-1 is PSPACE-complete, introduces a new proof technique involving agent states, and presents GADGETEER, a system for verifying gadget-based systems.

Contribution

It establishes the PSPACE-completeness of Push-1, extends motion planning frameworks with agent states, and develops GADGETEER for formal verification of gadget systems.

Findings

Push-1 is PSPACE-complete.

GADGETEER can verify gadget system behaviors.

Constructed a self-closing door example for verification.

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.