  This paper proposes a finitely terminating algorithm to solve reach-and-stay
control problems for nonlinear systems. The algorithm is guaranteed to return a
control strategy if the specification is robustly realizable. Such a feature is
desirable as the commonly used abstraction-based methods are sound but not
complete for systems that are not incrementally stable. Fundamental to the
proposed method is a fixed-point characterization of the winning set of the
system with respect to a given specification, i.e., the initial states that can
be controlled to satisfy the specification. The use of an adaptive partitioning
scheme not only guarantees the approximation precision of the winning set but
also reduces computational time. The effectiveness and efficiency are
illustrated by several benchmarking examples.
