  This paper deals with the control synthesis problem for a continuous
nonlinear dynamical system under a Linear Temporal Logic (LTL) formula. The
proposed solution is a top-down hierarchical decomposition of the control
problem involving three abstraction layers of the problem, iteratively solved
from the coarsest to the finest. The LTL planning is first solved on a small
transition system only describing the regions of interest involved in the LTL
formula. For each pair of consecutive regions of interest in the resulting
accepting path satisfying the LTL formula, a discrete plan is then constructed
in the partitioned workspace to connect these two regions while avoiding unsafe
regions. Finally, an abstraction refinement approach is applied to synthesize a
controller for the dynamical system to follow each discrete plan. The second
main contribution, used in the third abstraction layer, is a new
monotonicity-based method to over-approximate the finite-time reachable set of
any continuously differentiable system. The proposed framework is demonstrated
in simulation for a motion planning problem of a mobile robot modeled as a
disturbed unicycle.
