ABSTRACT
This chapter presents a direct approach for solving control synthesis problems with linear temporal logic specifications. As opposed to the abstraction-based approach, control synthesis algorithms are directly performed on the continuous state space of a dynamical system, by iteratively approximating controlled predecessors or one-step backward reachable sets. An interval branch-and-bound scheme is the computational engine for the precision-controlled under-approximations of controlled predecessors. This leads to the main result: a finitely terminating algorithm for solving a general class of linear temporal control synthesis problems if the specification is realizable for the nonlinear system even under small additive disturbances, which is called sound and robustly complete. The chapter presents such algorithms for both classical specifications such as invariance and reachability and more general specifications written as linear temporal logic formulas. The results are also extended to continuous-time systems with sample-and-hold control strategies. Complexity comparison with the abstraction-based approach is also provided as an insight to both formal control methods.
