Push-1 is PSPACE-complete, and the automated verification of motion planning gadgets
Zachary DeStefano, Bufang Liang

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 (a variant of Push-1 where the agent can push 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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
