  This paper proposes a specification-guided framework for control of nonlinear
systems with linear temporal logic (LTL) specifications. In contrast with
well-known abstraction-based methods, the proposed framework directly
characterizes the winning set, i.e., the set of initial conditions from which a
given LTL formula can be realized, over the continuous state space of the
system via a monotonic operator. Following this characterization, an algorithm
is proposed to practically approximate the operator via an adaptive interval
subdivision scheme, which yields a finite-memory control strategy. We show that
the proposed algorithm is sound for full LTL specifications, and robustly
complete for specifications recognizable by deterministic B\"uchi automata
(DBA), the latter in the sense that control strategies can be found whenever
the given specification can be satisfied with additional bounded disturbances.
Without having to compute and store the abstraction and the resulting product
system with the DBA, the proposed method is more memory efficient, which is
demonstrated by complexity analysis and performance tests. A pre-processing
stage is also devised to reduce computational cost via a decomposition of the
specification. We show that the proposed method can effectively solve
real-world control problems such as jet engine compressor control and motion
planning for manipulators and mobile robots.
