Push-1 是 PSPACE-complete，且运动规划小部件的自动化验证

Push-1 是最简单的抽象运动规划框架之一；然而，决定 Push-1 问题是否可解的复杂性长期以来是一个数十年的开放问题。我们通过表明 Push-1 是 PSPACE-complete 来解决了该运动规划问题的复杂性，并对我们的构造正确性进行形式化验证。我们的结果建立在最近一次工作的基础上，该工作表明 Push-1F（一种带有固定小块的 Push-1 变体）和 Push-k（其中 agent 同时推动 k 个小块的 Push-1 变体）对于 k \ge 2 是 PSPACE-complete，并且更一般地针对运动规划-小部件框架。为了解决这一开放问题，我们在运动规划复杂性理论中做出了两个一般性贡献。首先，我们的证明技术通过为 agent 分配状态来扩展标准运动规划框架。该状态在遍历小部件之间时保持不变，但可以在小部件中的转换时发生变化。其次，我们设计并实现了一个系统 GADGETEER，用于计算验证小部件系统的行为。该系统对底层运动规划问题是中性的，并且允许对低层构造与高层小部件系统之间的对应关系进行形式化验证，以及自动从低层构造中合成小部件。在 Push-1 的情况下，我们使用该系统形式化地证明我们的构造与其高层规范的行为相匹配。这 culminates 在构建和验证一个自闭式门的构造中，在自闭式门系统中决定可达性是 PSPACE-complete。