  This article presents an approach to encode Linear Temporal Logic (LTL)
Specifications into a Mixed Integer Quadratically Constrained Quadratic Program
(MIQCQP) footstep planner. We propose that the integration of LTL
specifications into the planner not only facilitates safe and desirable
locomotion between obstacle-free regions, but also provides a rich language for
high-level reasoning in contact planning. Simulations of the footstep planner
in a 2D environment satisfying encoded LTL specifications demonstrate the
results of this research.
