Signal Temporal Logic Meets Convex-Concave Programming:
A Structure-Exploiting SQP Algorithm for STL Specifications

Throughout this paper, we consider a discrete-time linear system:

$$x_{t+1}=Ax_{t}+Bu_{t},$$

(1)

where $A\in\mathbb{R}^{n\times n},B\in\mathbb{R}^{n\times m},$ and $x_{t}\in\mathcal{X}\subseteq\mathbb{R}^{n},u_{t}\in\mathcal{U}\subseteq$ $\mathbb{R}^{m}$ denote the state and input. We assume that $\mathcal{X}$ and $\mathcal{U}$ are a conjunction of polyhedra. Given an initial state $x_{0}\in\mathcal{X}$ and a sequence of control inputs $\boldsymbol{u}=(u_{0},\ldots,u_{T-1})$, the sequence of states $\boldsymbol{x}=(x_{0},\ldots,x_{T})$, which we call a trajectory, is uniquely generated.

In this study, we consider the specifications given in STL. STL is a predicate logic defined for specifying properties for continuous signals [1]. STL consists of predicates $\mu$ that can be obtained through a function $g^{\mu}(\cdot)$ as follows:

$$\mu=\begin{cases}\top\text{ if }g^{\mu}(\boldsymbol{x})\leq 0\\ \perp\text{ if }g^{\mu}(\boldsymbol{x})>0.\end{cases}$$

(2)

In this study, we consider affine functions for $g^{\mu}$ of the form $g^{\mu}=a^{\mathsf{T}}x_{t}-b:\mathcal{X}\rightarrow\mathbb{R}$, where $a\in\mathbb{R}^{n}$ and $b\in\mathbb{R}$. In addition to standard boolean operators $\wedge,\vee$, in STL, temporal operators $\square$ (always), $\Diamond$ (eventually), and $\boldsymbol{U}$ (until) are also considered. Each temporal operator has an associated bounded time interval $[t_{1},t_{2}]$ where $0\leq t_{1}<t_{2}<\infty$. We assume that STL formulae are written in negation normal form (NNF) without loss of generality [8]. STL formulae in NNF have negations only in front of the predicates [9] and we omit such negations from STL syntax. We refer to this negation-free STL as STL, which is defined by [10]:

$\displaystyle\varphi:=\mu|\vee\varphi|\wedge\varphi|\square_{\left[t_{1},t_{2}\right]}\varphi|\Diamond_{\left[t_{1},t_{2}\right]}\varphi\mid\varphi_{1}\boldsymbol{U}_{\left[t_{1},t_{2}\right]}\varphi_{2}.$

The notion of robustness is a useful semantic defined for STL formulae, which is a real-valued function that describes how much a trajectory satisfies an STL formula. Let $(\boldsymbol{x},t)$ denote a trajectory starting at timestep $t$, i.e., $(\boldsymbol{x},t)=x_{t},x_{t+1},...,x_{T}$. The trajectory length $T$ should be selected large enough to calculate the satisfaction of a formula (see e.g., [9]). Given an STL formula $\varphi$, we define the reversed robustness with respect to a trajectory $\boldsymbol{x}$ and a time $t$ that can be obtained recursively according to the following quantitative semantics:

Note that we define the recursive semantics for the reversed robustness function, i.e., the minus of the original robustness $\rho_{\text{orig}}^{\varphi}$ defined in the literature (see e.g., [11, Definition 2]) as $\rho_{\text{rev}}^{\varphi}=-\rho_{\text{orig}}^{\varphi}$. We reverse the sign of the robustness functions $\rho_{\text{rev}}^{\mu}$ of predicates $\mu$, and we interchange the $\max$ and $\min$ operators. The reversed-robustness function is introduced as a notational simplification within our robustness decomposition framework. This approach removes unfavorable minus sign symbols in the decomposition and establishes a correspondence between convex parts in the optimization and conjunctive operators in the specification, and similarly for concave parts. It is worth mentioning that this modification does not change all the properties of the original robustness as we simply reverse the signs in the definition of the robustness function.

STL can be represented as a tree [12, 13]. An example is shown below.

The robustness function that results from (3) is not differentiable due to the $\operatorname{\max}$ and $\operatorname{\min}$ operators, and thus, we cannot calculate the gradients of this function. Recent papers such as [4] smooth these functions in order to apply gradient-based methods. However, because smoothing both the $\max$ and $\min$ of the function leads to a problem that deviates from the original, it is preferable to minimize the parts that are smoothed. Our method requires to smooth only $\min$ functions. This is because $\max$ functions in the robustness are rather decomposed in our method as shown in Section III. The popular smooth approximation of the $\max$ and $\min$ operators is by using the log-sum-exp (LSE) function. This approximation for $\min$ operators is given as:

$$\overline{\min}_{k}(a_{1},...,a_{r}):=-\frac{1}{k}\ln\sum_{i=1}^{r}e^{-ka_{i}},$$

(5)

where $a_{i}\in\mathbb{R}$ and $k$ is the smooth parameter. Now, we define a new robustness measure that will be used throughout this paper.

This study considers the problem of synthesizing the trajectory that satisfies the STL specification in a maximally robust way. Given the system (1) and the specification $\varphi$ and the initial state $x_{0}$, the optimization problem is as follows:

	$\displaystyle\min_{\boldsymbol{x},\boldsymbol{u}}\hskip 5.0pt$	$\displaystyle\quad\overline{\rho}_{\text{rev}}^{\varphi}(\boldsymbol{x})$		(6a)
	s.t.	$\displaystyle x_{t+1}=Ax_{t}+Bu_{t}$		(6b)
		$\displaystyle x_{t}\in\mathcal{X},u_{t}\in\mathcal{U}$		(6c)
		$\displaystyle\overline{\rho}_{\text{rev}}^{\varphi}(\boldsymbol{x})\leq 0$		(6d)

Note that the reversed-robustness $\rho_{\text{rev}}^{\varphi}(\boldsymbol{x})$ is replaced with the smoothed reversed-robustness $\overline{\rho}_{\text{rev}}^{\varphi}(\boldsymbol{x})$ in (6a) and (6d). Thus, although a feasible solution of the non-smoothed problem always satisfies the specification (4), a feasible solution of (6) does not necessarily satisfy the specification (as it under-approximates the non-smoothed robustness). However, the approximation error can be made arbitrarily small by making the smooth parameter $k$ sufficiently large [4, 5].

The convex-concave procedure [6, 7] is a heuristic method for finding a local optimum of a class of optimization problems called the difference of convex (DC) programs, which is defined as follows:

The basic idea of CCP is simple; at each iteration of the optimization of the DC program (7), we replace concave terms with a convex upper bound obtained by linearization and then solve the resulting convex problem using convex optimization algorithms. It can be shown that all of the iterates are feasible if the starting point lies within the feasible set and the objective value converges (possibly to negative infinity, see [6, 14] for proof).

Note that either of the functions $p_{i}(\boldsymbol{z}),q_{i}(\boldsymbol{z})$ in equality constraints (8) are also approximated by the CCP. This is because an equality constraint is transformed into two inequalities (9) and both convex functions can make either inequality concave. Therefore, we should avoid introducing equality constraints if possible.

Our decomposition framework alters the problem into an efficient form of a DC program considering the aforementioned features of CCP-based algorithms. This decomposition not only transforms the problem into a DC program but also enhances the efficiency of the overall algorithm. As a result, the resulting program approximates only the truly concave parts, and our approach results in a new SQP method.

To this end, we need to know whether each function in the program (6) is convex or concave. In this program, the robustness function $\overline{\rho}_{\text{rev}}^{\varphi}$ is the only part whose curvature (convex or concave) cannot be determined. Thus, if the robustness function $\overline{\rho}_{\text{rev}}^{\varphi}$, which is a composite function consisting of $\max$ and $\min$ operators, can be rewritten as a combination of convex and concave functions, the entire program can be reduced to a DC program. The proposed framework achieves this by recursively decomposing the outermost operator of the robustness function until all the arguments of the functions are affine. As this study considers only affine functions for predicates $g^{\mu}(\cdot)$, if the arguments of a function are all predicates, the convexity or concavity of the function can be determined by examining the operator preceding it, which may be either a $\max$ or $\min$ function. The recursive decomposition of a nonconvex robustness function into predicates corresponds to a decomposition of the robustness tree from the top to the bottom, in accordance with the tree structure.

Our method utilizes the idea of the epigraphic reformulation methods. This method transforms the convex (usually linear) cost function into the corresponding epigraph constraints. However, our approach is different from the normal epigraphic reformulation in the sense that we deal with nonconvex cost functions and we have to apply the reformulation recursively. Our robustness decomposition transforms (6) into a more efficient form of DC program. To demonstrate our main idea, for the remainder of this paper, we use the simplified two-target specification described in Example 1 as the specification $\varphi$.

As the robustness function $\overline{\rho}_{\text{rev}}^{\varphi}$ is in the cost function, the first procedure is to decompose the function from the cost function into a set of constraints. As we consider the two-target specification, the outermost operator of the robustness function $\overline{\rho}_{\text{rev}}^{\varphi}$ is $\max$, i.e., $\overline{\rho}_{\text{rev}}^{\varphi}=\max(\overline{\rho}_{\text{rev}}^{\varphi_{1}},\overline{\rho}_{\text{rev}}^{\varphi_{2}},...,\overline{\rho}_{\text{rev}}^{\varphi_{r}})$. We introduce a new variable $s_{\xi}$, and reformulate the program as follows.

	$\displaystyle\min_{\boldsymbol{x},\boldsymbol{u},s_{\xi}}\hskip 1.99997pt$	$\displaystyle s_{\xi}$		(10a)
	s.t.	$\displaystyle x_{t+1}=Ax_{t}+Bu_{t}$		(10b)
		$\displaystyle x_{t}\in\mathcal{X},u_{t}\in\mathcal{U}$		(10c)
		$\displaystyle s_{\xi}\leq 0$		(10d)
		$\displaystyle\overline{\rho}_{\text{rev}}^{\varphi_{1}}\left(\boldsymbol{x}\right)\leq s_{\xi}\dots\overline{\rho}_{\text{rev}}^{\varphi_{r}}\left(\boldsymbol{x}\right)\leq s_{\xi}$		(10e)

Note that the set of inequalities (10e) is equivalent to

$$\max(\overline{\rho}_{\text{rev}}^{\varphi_{1}},\overline{\rho}_{\text{rev}}^{\varphi_{2}},...,\overline{\rho}_{\text{rev}}^{\varphi_{r}})\leq s_{\xi}$$

(11)

although the original semantics of the variable $s_{\xi}$ is the equality constraint:

$$\max(\overline{\rho}_{\text{rev}}^{\varphi_{1}},\overline{\rho}_{\text{rev}}^{\varphi_{2}},...,\overline{\rho}_{\text{rev}}^{\varphi_{r}})=s_{\xi}.$$

(12)

However, it is well known that this kind of $\max$ transformation is known to be equivalent, particularly for the convex case. Although (10) is nonconvex, we can also show that both (6) and (10) are equivalent (see [15] and [16, Section 8.3.4.4]). The proof of this equivalence is provided in Appendix -A for a later explanation (in particular (17)).

As each $\overline{\rho}_{\text{rev}}^{\varphi_{i}}$ for $i=1,\ldots,r$ is a robustness function, each inequality in (10e) can be restated as a constraint in one of the following two forms, depending on whether the outermost operator is $\max$ or $\min$:

	$\displaystyle\max(\overline{\rho}_{\text{rev}}^{\Phi_{1}},...,\overline{\rho}_{\text{rev}}^{\Phi_{y_{\max}}})\leq s_{\xi},$		(13)
	$\displaystyle\overline{\min}(\overline{\rho}_{\text{rev}}^{\Psi_{1}},...,\overline{\rho}_{\text{rev}}^{\Psi_{y_{\min}}})\leq s_{\xi},$		(14)

where functions $\overline{\rho}_{\text{rev}}^{\Phi_{j}}(j\in\{1,...,y_{\max}\})$ (resp. $\overline{\rho}_{\text{rev}}^{\Psi_{j}}(j\in\{1,...,y_{\min}\})$) are robustness functions associated with $\Phi_{j}$ (resp. $\Psi_{j}$), which are the subformulas of $\varphi_{i}(i\in\{1,...,r\})$. Note that these arguments of the $\max$ and $\min$ functions are still not necessarily predicates. We continue the following steps until all the arguments in each function become the predicates.

For inequality constraints of the form (13), we transform it as follows:

$\displaystyle\overline{\rho}_{\text{rev}}^{\Phi_{1}}\leq s_{\xi},\overline{\rho}_{\text{rev}}^{\Phi_{2}}\leq s_{\xi},...,\overline{\rho}_{\text{rev}}^{\Phi_{y_{\max}}}\leq s_{\xi}.$

(15)

This is of course equivalent to (13).

For constraints of the forms (14), we first check whether each argument of the $\overline{\min}$ function is a predicate or not. If not, we replace such an argument with a new variable. Because we consider the simplified two-target specification, the outermost operator of the function $\overline{\rho}_{\text{rev}}^{\Psi_{j}}(j\in\{1,...,y_{\min}\})$ is $\max$, i.e., $\overline{\rho}_{\text{rev}}^{\Psi_{j}}=\max(\overline{\rho}_{\text{rev}}^{\psi_{1}},...,\overline{\rho}_{\text{rev}}^{\psi_{h}})$. We first replace function $\overline{\rho}_{\text{rev}}^{\Psi_{j}}$ in (14) by a new variable $s_{\text{new}}$ as

$$\overline{\min}(\overline{\rho}_{\text{rev}}^{\Psi_{1}},...,s_{\text{new}},...,\overline{\rho}_{\text{rev}}^{\Psi_{y_{\min}}})\leq s_{\xi}.$$

(16)

Then, we add the following constraints:

$$\max(\overline{\rho}_{\text{rev}}^{\psi_{1}},...,\overline{\rho}_{\text{rev}}^{\psi_{h}})\leq s_{\text{new}}.$$

(17)

Although the inequality constraint (17) should be equality, this modification is justified by the similar discussion for (10e) even though the equivalence of this transformation is not immediately obvious (see the proof of Theorem 1).

All the inequalities in (15) and (17) are either in the $\max$ form (13) or the $\min$ form (14). Thus, subsequent to these steps, the constraints of the forms (13), (14) are decomposed into several constraints in the same forms again. We repeat this procedure until we reach the predicates, which is the bottom of the tree in Figure 2. When we finish the above recursive manipulations, (6) is transformed into an DC program as follows:

	$\displaystyle\min_{\boldsymbol{x},\boldsymbol{u},s_{\xi},\boldsymbol{s}_{\max},\boldsymbol{s}_{\min}}\hskip 1.99997pt$	$\displaystyle s_{\xi}$		(18a)
	s.t.	$\displaystyle x_{t+1}=Ax_{t}+Bu_{t}$		(18b)
		$\displaystyle x_{t}\in\mathcal{X},u_{t}\in\mathcal{U}$		(18c)
		$\displaystyle s_{\xi}\leq 0,$		(18d)
		$\displaystyle\left.\begin{tabular}[]{l}$\overline{\rho}_{\text{rev}}^{\lambda^{(1)}_{1}}\leq s^{(1)}_{\max},...,\overline{\rho}_{\text{rev}}^{\lambda^{(1)}_{y_{\max}}}\leq s^{(1)}_{\max}$\\ $\quad\quad\vdots\hskip 71.13188pt\vdots$\\ $\overline{\rho}_{\text{rev}}^{\lambda^{(v)}_{1}}\leq s^{(v)}_{\max},...,\overline{\rho}_{\text{rev}}^{\lambda^{(v)}_{y_{\max}}}\leq s^{(v)}_{\max}$\\ \end{tabular}\right\}\begin{tabular}[]{l}\text{from }$\max$\\ \text{functions}\end{tabular}$		(18j)
		$\displaystyle\left.\begin{tabular}[]{l}$\overline{\min}(\overline{\rho}_{\text{rev}}^{\mu^{(1)}_{1}},...,\overline{\rho}_{\text{rev}}^{\mu^{(1)}_{y_{\min}}})\leq s^{(1)}_{\min}$\\ $\quad\quad\vdots$\\ $\overline{\min}(\overline{\rho}_{\text{rev}}^{\mu^{(w)}_{1}},...,\overline{\rho}_{\text{rev}}^{\mu^{(w)}_{y_{\min}}})\leq s^{(w)}_{\min},$\\ \end{tabular}\right\}\begin{tabular}[]{l}\text{from }$\min$\\ \text{functions}\end{tabular}$		(18p)

where all the formulas $\lambda_{1}^{(\cdot)},...,\lambda_{y_{\max}}^{(\cdot)},\mu_{1}^{(\cdot)},...,\mu_{y_{\min}}^{(\cdot)}$ in (18j) and (18p) are predicates and $\boldsymbol{s}_{\max}=(s^{(1)}_{\max},...,s^{(v)}_{\max})$ and $\boldsymbol{s}_{\min}=(s^{(1)}_{\min},...,s^{(w)}_{\min})$. Note that, with some abuse of notation, some variables in $\boldsymbol{s}_{\max},\boldsymbol{s}_{\min}$ in constraints (18j),(18p) may represent $s_{\xi}$ and $s_{\text{new}}$, and some arguments of the $\overline{\min}$ function in (18p) are not affine predicates but the new variables.

Important properties of this program (18) are stated below.