  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.
