Integer-Free Control Synthesis for Signal Temporal Logic via Ranked Implicants

Abstract

This paper proposes an integer-free method for control synthesis of nonlinear discrete-time systems under finite-horizon Signal Temporal Logic (STL) constraints. Instead of introducing integer variables, we consider the discrete choices of the specification in a ranked order and solve a standard nonlinear program for each selected choice until a satisfying trajectory is found. We first define implicants as sets of timed atomic constraints whose joint satisfaction is sufficient to satisfy the specification. A reference trajectory obtained from a smooth approximation of the STL robustness is used to rank these implicants. Fixing one implicant turns the problem into a standard nonlinear program with no auxiliary weights or bilinear terms. If the solution does not satisfy the specification, the next implicant will be considered. We prove soundness and completeness of our method relative to the nonlinear programming solver. Numerical evaluation on nonlinear multi-agent systems shows that our proposed method identifies satisfying trajectories where the exact continuous reformulation fails, and moreover, it is faster than a mixed-integer formulation of the same specification.