论文标题
强大的反例引导的优化，用于从可区分的时间逻辑进行计划
Robust Counterexample-guided Optimization for Planning from Differentiable Temporal Logic
论文作者
论文摘要
信号时间逻辑（STL）提供了一个强大的灵活框架，用于指定复杂的自主任务；但是，基于STL规范的现有计划方法难以扩展到长途任务，并且不适合外部干扰。在本文中，我们提出了一种算法，用于查找满足STL规格的强大计划。我们的方法在局部优化和本地伪造之间进行了交替，使用自动区分的时间逻辑来迭代地对其计划进行优化，以响应在伪造过程中发现的反例。我们针对两个长胜卫星会合任务的最先进的计划方法进行了反示例引导计划方法，这表明我们的方法找到了尽管有对抗性干扰，但仍满足STL规格的高质量计划。我们发现我们的方法始终找到对对抗性干扰的计划，并且需要竞争方法的一半以下。我们在https://github.com/mit-realm/architect上提供了计划者的实现。
Signal temporal logic (STL) provides a powerful, flexible framework for specifying complex autonomy tasks; however, existing methods for planning based on STL specifications have difficulty scaling to long-horizon tasks and are not robust to external disturbances. In this paper, we present an algorithm for finding robust plans that satisfy STL specifications. Our method alternates between local optimization and local falsification, using automatically differentiable temporal logic to iteratively optimize its plan in response to counterexamples found during the falsification process. We benchmark our counterexample-guided planning method against state-of-the-art planning methods on two long-horizon satellite rendezvous missions, showing that our method finds high-quality plans that satisfy STL specifications despite adversarial disturbances. We find that our method consistently finds plans that are robust to adversarial disturbances and requires less than half the time of competing methods. We provide an implementation of our planner at https://github.com/MIT-REALM/architect.
