Graph-Based Convexification of Nested Signal Temporal Logic Constraints for Trajectory Optimization

In the above STL Eqs. (4) to (9), the result is a Boolean: either the property is True, or False. In order to gain more insight, a margin function is introduced to better classify an STL expression. The margin function $\rho$ defines the truth of the STL formula as shown in Fig. 1. This margin function is computed using minimum and maximum functions for the STL operators introduced in Table 1 and used in Eqs. (4) to (9).

Let us consider a practical example to better illustrate the interest of the margin function $\rho$. By denoting the position of an autonomous system as $\bm{r}$, the condition $\lVert\bm{r}(t)\rVert\geq d$ states that at time $t$ the system remains at a distance greater than a certain value $d$ from an obstacle located at the reference frame’s origin. In that case, defining a margin function such that $\rho(t)=\lVert\bm{r}(t)\rVert-d$, the security condition is satisfied at time t if and only if $\rho$ is positive at $t$. STL formulas (4) to (9) can be expressed as follows, in terms of margin semantics using margin functions.

The complete robust semantics for Eq. (4) is given by:

$$\rho^{\pi^{\mu}}_{k}=\mu(\bm{x}_{k},\bm{u}_{k}).$$

(10)

Margin function for the negation of a property $\psi$ of the Eq. (5) is given by:

$$\rho^{\neg\psi}_{k}=-\rho^{\psi}_{k}.$$

(11)

Margin function of Eq. (6) as conjunction satisfies the following minimum property in terms of margin functions of $\varphi$ and $\psi$:

$$\rho^{\varphi\wedge\psi}_{k}=\min(\rho^{\varphi}_{k},\rho^{\psi}_{k}).$$

(12)

Instead, margin function of Eq. (7) as disjunction satisfies the following maximum property in terms or margin functions of $\varphi$ and $\psi$:

$$\rho^{\varphi\lor\psi}_{k}=\max(\rho^{\varphi}_{k},\rho^{\psi}_{k}).$$

(13)

Margin function of Eq. (8) (involving constraint Eventually ($\diamond$) $\varphi$ True between time $a$ and $b$) is positive when the maximum of the constraint margin function is positive in the interval:

$$\rho^{\diamond_{[a,b]}\varphi}=\max\limits_{k\in[a,b]}\rho^{\varphi}_{k}.$$

(14)

Margin function of Eq. (9) (involving constraint Always ($\Box$) $\varphi$ True between time $a$ and $b$) is positive when the minimum of the constraint margin function is positive in the interval:

$$\rho^{\square_{[a,b]}{\varphi}}=\min\limits_{k\in{[a,b]}}\rho^{\varphi}_{k}.$$

(15)

As it was seen in Section 2.1.1, the margin of the operators are functions of time and derived from $min$ and $max$ functions. So, to model this in the discrete world, new variables (scalars), denoted as STL-variables, representing the margin (which is a scalar) evaluated at each time step, are introduced:

$$\bm{\alpha}=\left[\begin{array}[]{c}\alpha_{1}\\ \vdots\\ \alpha_{N}\end{array}\right].$$

(16)

The STL-variable vector augments the state vector of the optimization variables:

$$\bm{x}=\left[\begin{array}[]{c}\bm{x}_{1}\\ \vdots\\ \bm{x}_{N}\end{array}\right],$$

(17)

to give:

$$\bm{z}=\left[\begin{array}[]{c}\bm{x}\\ \hline\cr\bm{\alpha}\end{array}\right].$$

(18)

The goal is to replicate the behavior of the max or min functions over time intervals $[a,b]$. The extremum is initialized at the first value of the interval and propagates through it. The obtained value at the end of the interval is kept until the end. It follows:

$$\left\{\begin{matrix}\begin{array}[]{ll}\alpha_{k}=\rho^{\varphi}_{k_{a}}\\ \alpha_{k+1}=\chi(\alpha_{k},\rho^{\varphi}_{k+1})\\ \alpha_{k}=\alpha_{k_{b}}\end{array}&\begin{array}[]{ll}\forall k=1,\dots,k_{a}\\ \forall k=k_{a},\dots,k_{b}-1\\ \forall k=k_{b}+1,\dots,N\end{array}\end{matrix}\right.,$$

(19)

where $\chi$ is a general function representing the margin, e.g., functions $min$ or $max$.

Between times $a$ and $b$, the STL-variable vector $\bm{\alpha}$ is now defined as a sequence of scalar variables $(\alpha_{k})_{(k_{a}:k_{b})}$ following the discrete dynamics:

$$\alpha_{k+1}=\chi(\alpha_{k},\rho^{\varphi}_{k+1}).$$

(20)

The margin function, in turn, depends on the dynamics of the system under control:

$$\rho^{\varphi}_{k+1}=\rho^{\varphi}_{k+1}\left(\bm{x}_{k+1}\right).$$

(21)

Now, the STL-variables are defined over the whole time horizon to follow the continuous definition of the margin function. In particular, the functions $min$ and $max$ are not linear as function of the other STL-variables, not even differentiable (indeed the maximum and minimum function have sharp edges at the flips). Function $\rho^{\varphi}$ is in general not linear as well (e.g. when asking for a distance between an object and an obstacle being greater that a threshold, the norm function is involved). These kinds of functions are not straightforwardly implementable in a standard convex optimization algorithm. A linearization step is then performed to cope with this framework.

Let us assume that function $\chi$ is differentiable. In that case, it would be desired to consider the STL-variables appearing linearly to build a linear system of equations. Using the chain rule (derivation of function composition), the approximation to the first order of the Taylor expansion leads:

$$\alpha_{k+1}=\chi(\alpha_{k},\rho^{\varphi}_{k+1})\approx\chi(\bar{\alpha}_{k},\bar{\rho}^{\varphi}_{k+1})+\left.\frac{\partial\chi}{\partial\alpha_{k}}\right|_{\bar{\alpha}_{k},\bar{\rho}^{\varphi}_{k+1}}(\alpha_{k}-\bar{\alpha}_{k})+\left.\frac{\partial\chi}{\partial\rho^{\varphi}_{k+1}}\right|_{\bar{\alpha}_{k},\bar{\rho}^{\varphi}_{k+1}}\left.\frac{\partial\rho^{\varphi}_{k+1}}{\partial\bm{x}_{k+1}}\right|_{\bar{\bm{x}}_{k+1}}(\bm{x}_{k+1}-\bar{\bm{x}}_{k+1}),$$

(22)

where the notation $\bar{x}_{j}$ for any general variable $x$ represents the reference of $x$ at time $j$ (e.g. either of the initialization or the last optimal iteration). Introducing the zero order term:

$$R(\bar{\alpha}_{k},\bar{\bm{x}}_{k+1})=\chi(\bar{\alpha}_{k},\bar{\rho}^{\varphi}_{k+1})-\left.\frac{\partial\chi}{\partial\alpha_{k}}\right|_{\bar{\alpha}_{k},\bar{\rho}^{\varphi}_{k+1}}\bar{\alpha}_{k}-\left.\frac{\partial\chi}{\partial\rho^{\varphi}_{k+1}}\right|_{\bar{\alpha}_{k},\bar{\rho}^{\varphi}_{k+1}}\left.\frac{\partial\rho^{\varphi}_{k+1}}{\partial\bm{x}_{k+1}}\right|_{\bar{\bm{x}}_{k+1}}\bar{\bm{x}}_{k+1},$$

(23)

Dropping the reference notation for the gradients in the following part of the paper, for the sake of conciseness, one finally gets:

$$\alpha_{k+1}=R(\bar{\alpha}_{k},\bar{\bm{x}}_{k+1})+\frac{\partial\chi}{\partial\alpha_{k}}\alpha_{k}+\frac{\partial\chi}{\partial\rho^{\varphi}_{k+1}}\frac{\partial\rho^{\varphi}_{k+1}}{\partial\bm{x}_{k+1}}\bm{x}_{k+1}.$$

(24)

Equation (24) is now linear in the STL-variables $\bm{\alpha}$ and in the dynamic state variables $\bm{z}$. Function $\chi$, when equal to $min$ or $max$, is not differentiable. However, as proposed in [MAGC22], it can be approximated with smoothed functions ($smin$ and $smax$ for $min$ and $max$ respectively). Function $smin$ and $smax$ are defined as follows (see also Fig. 2 depicting an example):

$$smin(a,b,\kappa)=\left\{\begin{matrix}\begin{array}[]{ll}b\\ a\\ g_{min}(a,b,\kappa)\end{array}&\begin{array}[]{ll}\mathrm{if}\\ \mathrm{if}\\ \mathrm{if}\end{array}&\begin{array}[]{ll}a-b\geq\kappa\\ a-b\leq-\kappa\\ a-b\in[-\kappa,\dots,\kappa]\end{array}\end{matrix}\right.,$$

(25)

where $g_{min}$ is the smoothing function:

$$\begin{matrix}g_{min}(a,b,\kappa)=a(1-h)+hb-\kappa h(1-h),&\mathrm{with}&h=\frac{1}{2}+\frac{a-b}{2\kappa}\end{matrix},$$

(26)

dependent on its smoothing gain $\kappa$.

As stated in Eq. (24), partial derivatives of the margin functions are essential to define the STL-variable dynamics:

$$\frac{\partial smin}{\partial a}(a,b,\kappa)=\left\{\begin{matrix}\begin{array}[]{ll}0\\ 1\\ 1-h\end{array}&\begin{array}[]{ll}\mathrm{if}\\ \mathrm{if}\\ \mathrm{if}\end{array}&\begin{array}[]{ll}a-b\geq\kappa\\ a-b\leq-\kappa\\ a-b\in[-\kappa,\dots,\kappa]\end{array}\end{matrix}\right.,$$

(27)

$$\frac{\partial smin}{\partial b}(a,b,\kappa)=\left\{\begin{matrix}\begin{array}[]{ll}1\\ 0\\ h\end{array}&\begin{array}[]{ll}\mathrm{if}\\ \mathrm{if}\\ \mathrm{if}\end{array}&\begin{array}[]{ll}a-b\geq\kappa\\ a-b\leq-\kappa\\ a-b\in[-\kappa,\dots,\kappa]\end{array}\end{matrix}\right..$$

(28)

Caution has to be taken by the reader since $smin\neq-smax$. Indeed, function $smax$ is defined as:

$$smax(a,b,\kappa)=\left\{\begin{matrix}\begin{array}[]{ll}b\\ a\\ g_{max}(a,b,\kappa)\end{array}&\begin{array}[]{ll}\mathrm{if}\\ \mathrm{if}\\ \mathrm{if}\end{array}&\begin{array}[]{ll}b-a\geq\kappa\\ b-a\leq-\kappa\\ b-a\in[-\kappa,\dots,\kappa]\end{array}\end{matrix}\right.,$$

(29)

where $g_{max}$ is the smoothing function:

$$\begin{matrix}g_{max}(a,b,\kappa)=b(1-h)+ha+\kappa h(1-h),&\mathrm{with}&h=\frac{1}{2}+\frac{a-b}{2\kappa}\end{matrix},$$

(30)

dependent on its smoothing gain $\kappa$.

Partial derivatives of the margin function $smax$ are the following:

$$\frac{\partial smin}{\partial a}(a,b,\kappa)=\left\{\begin{matrix}\begin{array}[]{ll}0\\ 1\\ h\end{array}&\begin{array}[]{ll}\mathrm{if}\\ \mathrm{if}\\ \mathrm{if}\end{array}&\begin{array}[]{ll}b-a\geq\kappa\\ b-a\leq-\kappa\\ b-a\in[-\kappa,\dots,\kappa]\end{array}\end{matrix}\right.,$$

(31)

$$\frac{\partial smin}{\partial b}(a,b,\kappa)=\left\{\begin{matrix}\begin{array}[]{ll}1\\ 0\\ 1-h\end{array}&\begin{array}[]{ll}\mathrm{if}\\ \mathrm{if}\\ \mathrm{if}\end{array}&\begin{array}[]{ll}b-a\geq\kappa\\ b-a\leq-\kappa\\ b-a\in[-\kappa,\dots,\kappa]\end{array}\end{matrix}\right..$$

(32)

These partial derivatives will allow to implement the derivatives of $\chi=\{min,max\}$ with respect to its variables as seen in (24).

In cases where the margin functions might not be differentiable at certain points (e.g., the norm function is not differentiable at 0), a null gradient can, for instance, be automatically introduced when performing the computation at these singular points. Of course, the smaller the $\kappa$, the better the approximation (in practice, not thinking about differentiability, $\kappa=0$ seemed of no concern in this work). Maybe some edge cases could be found in highly nonlinear settings, but with a usual step size, the vicinity of the flips is rarely, not to say never, encountered in practical applications. The takeaway is probably that that there is a parameter which can smoothen the dynamics if needed. In the following, the $\kappa$ input of $\chi$ will be omitted for conciseness.

After discretizing and linearizing the robust semantics of the STL-formulas, the final step is to transform the STL-variable dynamics equations into a convex matrix form of type $\bm{Az}=\bm{b}$, where:

• •

  $\bm{A}$ is defined as the state-transition matrix;

• •

  $\bm{z}$ is the augmented optimization vector composed of the state optimization variable vector $\bm{x}$ and of the STL-variable vector $\bm{\alpha}$);

• •

  $\bm{b}$ is the vector independent on the optimization variables.

To define these three convex framework elements on the basis of the discrete and linearized dynamics of Eqs (19) and (24), the following mathematical notation are used:

• •

  $\bm{I}_{K}$ is an identity square matrix of size $K$;

• •

  $\bm{0}_{K}$ is a column vector of length $K$ with all its elements equal to 0;

• •

  $\bm{0}_{K_{1},K_{2}}$ is a zero matrix with $K_{1}$ rows and $K_{2}$ columns;

• •

  $\bm{1}_{K}$ is a column vector of length $K$ with all its elements equal to 1;

• •

  $\mathrm{diag}\left(\left[\begin{matrix}u_{1}\dots u_{m}\end{matrix}\right]\right)_{K}$ is a diagonal concatenation of $K$ blocks, each equal to the row vector $\left[\begin{matrix}u_{1}\dots u_{m}\end{matrix}\right]$;

• •

  $\mathrm{diag}\left(\left[f(v_{1k}),\dots f(v_{mk})\right]\right)_{K_{1}:K_{2}}$ is a diagonal concatenation of $K_{2}-K_{1}+1$ blocks, equal to $\left[f(v_{1k}),\dots f(v_{mk})\right]$ for $k=K_{1},\dots,K_{2}$.

Compact convex formulation $\bm{Az}=\bm{b}$ is based on the following definitions:

1. 1.

   For matrix $\bm{A}$:

   $$\bm{A}=\left[\begin{array}[]{ccc|ccc}\bm{0}_{k_{a},k_{a}}&\bm{0}_{k_{a},k_{b}-k_{a}}&\bm{0}_{k_{a},N-k_{b}}&\bm{I}_{k_{a}}&\bm{0}_{k_{a},k_{b}-k_{a}}&\bm{0}_{k_{a},N-k_{b}}\\ \bm{0}_{k_{b}-k_{a},k_{a}}&\bm{A_{22}}&\bm{0}_{k_{b}-k_{a},N-k_{b}}&\bm{0}_{k_{b}-k_{a},k_{a}}&\bm{A_{25}}&\bm{0}_{k_{b}-k_{a},N-k_{b}}\\ \bm{0}_{N-k_{b},k_{a}}&\bm{0}_{N-k_{b},k_{b}-k_{a}}&\bm{0}_{N-k_{b},N-k_{b}}&\bm{0}_{N-k_{b},k_{a}}&\bm{0}_{N-k_{b},k_{b}-k_{a}}&\bm{A_{36}}\end{array}\right],$$

   (33)

   with:

   $$\bm{A_{22}}=\mathrm{diag}\left(\left[\frac{\partial\chi}{\partial\rho^{\varphi}_{k+1}}\frac{\partial\rho^{\varphi}_{k+1}}{\partial\bm{x}^{\varphi}_{k+1}}\right]\right)_{k_{a}:k_{b}-1},$$

   (34)

   $$\bm{A_{25}}=\mathrm{diag}\left(\left[\begin{matrix}\frac{\partial\chi}{\partial\alpha_{k}}&-1\end{matrix}\right]\right)_{k_{a}:k_{b}-1},$$

   (35)

   $$\bm{A_{36}}=\mathrm{diag}\left(\left[\begin{matrix}1&-1\end{matrix}\right]\right)_{N-k_{b}}.$$

   (36)

2. 2.

   For vector $\bm{z}$:

   $$\bm{z}=\left[\begin{array}[]{c}\bm{x}^{\varphi}\\ \hline\cr\bm{\alpha}\end{array}\right].$$

   (37)

3. 3.

   For vector $\bm{b}$:

   $$\bm{b}=\begin{bmatrix}\bar{\rho}^{\varphi}_{k_{a}}\bm{1}_{k_{a}}\\ -\mathrm{diag}\left(\left[R(\bar{\alpha}_{k},\bar{\bm{x}}^{\varphi}_{k+1})\right]\right)_{k_{a}:k_{b}-1}\bm{1}_{k_{b}-k_{a}}\\ \bm{0}_{N-k_{b}}\end{bmatrix}.$$

   (38)

This linear system of equations can then be concatenated with the other physical dynamics linear constraints to obtain an augmented optimization problem, which will then be fed to the convex optimization solver (e.g., second-order cone, semi-definite).

Finally, it remains a very last constraint, which is actually the most natural and important. Let us recall that the STL constraint will be satisfied if and only if the margin function is positive. This can be enforced by asking the last time step of the STL variable to be positive:

$$\alpha_{N}\geq 0.$$

(39)

Note that all the constraints are made to specifically arrive to this one.

Let $\varphi$ and $\psi$, be two predicates. The conjunction operator between $\varphi$ and $\psi$ is shown in Fig. 3, represented by a graph.

In terms of robust STL semantics, the margin function of the conjunction operator can be expressed as a minimum function:

$$min(\rho^{\varphi},\rho^{\psi}).$$

(40)

The discretization gives

$$\alpha_{k+1}=min(\rho^{\varphi}_{k+1},\rho^{\psi}_{k+1}),\;\;\;\forall k=0,1,\dots,N-1.$$

(41)

Defining as $\bm{x}^{\varphi}$ (respectively $\bm{x}^{\psi}$) the state variable vector used to write predicate $\varphi$ (respectively $\psi$), the linearization provides:

$$\alpha_{k+1}=R(\bar{\bm{x}}^{\varphi}_{k+1},\bar{\bm{x}}^{\psi}_{k+1})+\frac{\partial smin}{\partial\rho^{\varphi}_{k+1}}\frac{\partial\rho^{\varphi}_{k+1}}{\partial\bm{x}^{\varphi}_{k+1}}\;\bm{x}^{\varphi}_{k+1}+\frac{\partial smin}{\partial\rho^{\psi}_{k+1}}\frac{\partial\rho^{\psi}_{k+1}}{\partial\bm{x}^{\psi}_{k+1}}\bm{x}^{\psi}_{k+1}.$$

(42)

In general, the states considered by the two margin functions are completely different. For instance, one could use the positions, while the other one the attitude. In that case, they would have to be positioned differently in the STL matrix $\bm{A}$, easily made with an automated routine.

The terms of the compact convex formulation $\bm{Az}=\bm{b}$ becomes:

1. 1.

   For matrix $\bm{A}$:

   $$\bm{A}=\begin{bmatrix}\begin{array}[]{c|c|c}\mathrm{diag}\left(\left[\frac{\partial smin}{\partial\rho^{\varphi}_{k+1}}\frac{\partial\rho^{\varphi}_{k+1}}{\partial\bm{x}^{\varphi}_{k+1}}\right]\right)_{0:N-1}&\mathrm{diag}\left(\left[\frac{\partial smin}{\partial\rho^{\psi}_{k+1}}\frac{\partial\rho^{\psi}_{k+1}}{\partial\bm{x}^{\psi}_{k+1}}\right]\right)_{0:N-1}&-\bm{I}_{N}\end{array}\end{bmatrix},$$

   (43)

2. 2.

   For vector $\bm{z}$:

   $$\bm{z}=\left[\begin{array}[]{c}\bm{x}^{\varphi}\\ \hline\cr\bm{x}^{\psi}\\ \hline\cr\bm{\alpha}\end{array}\right],$$

   (44)

3. 3.

   For vector $\bm{b}$:

   $$\bm{b}=-\mathrm{diag}\left(\left[R(\bar{\bm{x}}^{\varphi}_{k+1},\bar{\bm{x}}^{\psi}_{k+1})\right]\right)_{0:N-1}\bm{1}_{N}.$$

   (45)

Taking the analogy with electric circuits, the system would look like Fig. 4:

Let $\varphi$ and $\psi$, be two predicates. The disjunction operator between $\varphi$ and $\psi$ is shown in Fig. 3, represented by a graph.

In terms of robust STL semantics, the margin function of the disjunction operator can be expressed as a maximum function:

$$max(\rho^{\varphi},\rho^{\psi}).$$

(46)

The discretization gives:

$$\alpha_{k+1}=max(\rho^{\varphi}_{k+1},\rho^{\psi}_{k+1}),\;\;\;\forall k=0,1,\dots,N-1.$$

(47)

Defining as $\bm{x}^{\varphi}$ (respectively $\bm{x}^{\psi}$) the state variable vector used to write predicate $\varphi$ (respectively $\psi$), the linearization provides:

$$\alpha_{k+1}=R(\bar{\bm{x}}^{\varphi}_{k+1},\bar{\bm{x}}^{\psi}_{k+1})+\frac{\partial smax}{\partial\rho^{\varphi}_{k+1}}\frac{\partial\rho^{\varphi}_{k+1}}{\partial\bm{x}^{\varphi}_{k+1}}\;\bm{x}^{\varphi}_{k+1}+\frac{\partial smax}{\partial\rho^{\psi}_{k+1}}\frac{\partial\rho^{\psi}_{k+1}}{\partial\bm{x}^{\psi}_{k+1}}\bm{x}^{\psi}_{k+1}.$$

(48)

In general, the states considered by the two margin functions are completely different. For instance, one could use the positions, while the other one the attitude. In that case, they would have to be positioned differently in the STL matrix $\bm{A}$, easily made with an automated routine.

The terms of the compact convex formulation $\bm{Az}=\bm{b}$ becomes:

1. 1.

   For matrix $\bm{A}$:

   $$\bm{A}=\begin{bmatrix}\begin{array}[]{c|c|c}\mathrm{diag}\left(\left[\frac{\partial smax}{\partial\rho^{\varphi}_{k+1}}\frac{\partial\rho^{\varphi}_{k+1}}{\partial\bm{x}^{\varphi}_{k+1}}\right]\right)_{0:N-1}&\mathrm{diag}\left(\left[\frac{\partial smax}{\partial\rho^{\psi}_{k+1}}\frac{\partial\rho^{\psi}_{k+1}}{\partial\bm{x}^{\psi}_{k+1}}\right]\right)_{0:N-1}&-\bm{I}_{N}\end{array}\end{bmatrix},$$

   (49)

2. 2.

   For vector $\bm{z}$:

   $$\bm{z}=\left[\begin{array}[]{c}\bm{x}^{\varphi}\\ \hline\cr\bm{x}^{\psi}\\ \hline\cr\bm{\alpha}\end{array}\right],$$

   (50)

3. 3.

   For vector $\bm{b}$:

   $$\bm{b}=-\mathrm{diag}\left(\left[R(\bar{\bm{x}}^{\varphi}_{k+1},\bar{\bm{x}}^{\psi}_{k+1})\right]\right)_{0:N-1}\bm{1}_{N}.$$

   (51)

Taking the analogy with electric circuits, the system would look like Fig. 6:

The Always operator is an operator of flow type, it asks for a property to always be True inside of a time window, which can cover the whole simulation. The Always operator is shown in Fig. 7 represented by a graph.

In terms of robust STL semantics, the margin function of this operator can be seen as a recurrent conjunction active at each time step of the time window. The discretization of this operator gives:

$$\left\{\begin{matrix}\begin{array}[]{ll}\alpha_{k}=\rho^{\varphi}_{k_{a}}\\ \alpha_{k+1}=\min(\alpha_{k},\rho^{\varphi}_{k+1})\\ \alpha_{k}=\alpha_{k_{b}}\end{array}&\begin{array}[]{ll}\forall k=1,\dots,k_{a}\\ \forall k=k_{a},\dots,k_{b}-1\\ \forall k=k_{b}+1,\dots,N\end{array}\end{matrix}\right.,$$

(52)

The terms of the compact convex formulation $\bm{Az}=\bm{b}$ have the same expression as the ones in Eqs (33)-(38) with:

$$\bm{A_{22}}=\mathrm{diag}\left(\left[\frac{\partial smin}{\partial\rho^{\varphi}_{k+1}}\frac{\partial\rho^{\varphi}_{k+1}}{\partial\bm{x}^{\varphi}_{k+1}}\right]\right)_{k_{a}:k_{b}-1},$$

(53)

$$\bm{A_{25}}=\mathrm{diag}\left(\left[\begin{matrix}\frac{\partial smin}{\partial\alpha_{k}}&-1\end{matrix}\right]\right)_{k_{a}:k_{b}-1}.$$

(54)

Taking the analogy with electric circuits, the system would look like Fig. 8.

The Eventually operator is an operator of flow type, it asks for a property to be True at least once inside of a time window, which can cover the whole simulation. The Eventually operator is shown in Fig. 9 represented by a graph.

In terms of robust STL semantics, the margin function of this operator can be seen as a recurrent disjunction active at each time step of the time window. The discretization of this operator gives:

$$\left\{\begin{matrix}\begin{array}[]{ll}\alpha_{k}=\rho^{\varphi}_{k_{a}}\\ \alpha_{k+1}=\max(\alpha_{k},\rho^{\varphi}_{k+1})\\ \alpha_{k}=\alpha_{k_{b}}\end{array}&\begin{array}[]{ll}\forall k=1,\dots,k_{a}\\ \forall k=k_{a},\dots,k_{b}-1\\ \forall k=k_{b}+1,\dots,N\end{array}\end{matrix}\right..$$

(55)

The terms of the compact convex formulation $\bm{Az}=\bm{b}$ have the same expression of Eqs (33)-(38) with:

$$\bm{A_{22}}=\mathrm{diag}\left(\left[\frac{\partial smax}{\partial\rho^{\varphi}_{k+1}}\frac{\partial\rho^{\varphi}_{k+1}}{\partial\bm{x}^{\varphi}_{k+1}}\right]\right)_{k_{a}:k_{b}-1},$$

(56)

$$\bm{A_{25}}=\mathrm{diag}\left(\left[\begin{matrix}\frac{\partial smax}{\partial\alpha_{k}}&-1\end{matrix}\right]\right)_{k_{a}:k_{b}-1}.$$

(57)

Taking the analogy with electric circuits, the system would look like Fig. 10.

A very important aspect of general nesting is how the margin function is transmitted from each operator to the next one above it. In the previous section, when dealing with a single operator, a forward propagation of the STL variables was performed (i.e., $\alpha_{k+1}=\chi(\alpha_{k},\rho^{\varphi}_{k+1}))$. In the general case, with nesting operators, backward propagation plays a major role in preventing loss of information. To visualize the concept, let us consider the following nesting example:

$$\underset{\beta}{\diamond}(\underset{\alpha}{\Box}\varphi),$$

(64)

represented in Fig. 13, where the notations $\alpha$ and $\beta$ are the STL variables associated to their respective operators. To illustrate the concept, let assume that the example result is True during the last two time steps, i.e., margin function $\rho^{\varphi}$ is eventually always positive for these steps. As always, the STL variable at the last time step must be positive. One notices that the backward propagation of the margins preserves the Boolean conclusion (i.e., the property is True), information being lost at the first negative value in case of forward propagating due to the nesting of $min$ and $max$ functions.

Another more complex nesting will be presented in Sec. 4.3.2 to build up intuition before presenting the general rules in Sec. 4.3.3.

Until operator, represented with notation $\varphi\mathcal{U}\psi$, and as presented in [MAGC22], is an operator that checks if a predicate $\varphi$ is always True when another predicate $\psi$ triggered True. When taking a closer look at it, $\mathcal{U}$ can be constructed as a nesting of basic operators and written as follows:

$$\varphi\mathcal{U}\psi\equiv\diamond(\psi\wedge\Box\varphi).$$

(65)

On the other hand, when one reads the sentence When $\psi$ would trigger True, $\varphi$ had to have always been True before, a notion of the history of $\varphi$ appears. Therefore, one can state that $\mathcal{U}$ is specifically interested in the history of $\varphi$. For this reason, the Until operator could be constructed also as follows

$$\varphi\mathcal{U}\psi\equiv\diamond(\psi\wedge\Box^{\mathcal{B}}\varphi),$$

(66)

New notation are introduced to take into account temporal direction in the property validity and in the propagation

• •

  $\Box^{\mathcal{B}}$ indicates Always before;

• •

  $\Box^{\mathcal{A}}$ indicates Always after;

• •

  $\bm{\alpha}^{\rightarrow}$ indicates that STL variable $\bm{\alpha}$ is propagated forward because interested in the past (case of all of what has been done in this paper so far as well as in [MAGC22]);

• •

  $\bm{\alpha}^{\leftarrow}$ indicates that STL variable $\bm{\alpha}$ is propagated backward because interested in the future.

Another example using Until operator is depicted in Fig. 14 and represented as follows:

$$\varphi\mathcal{U}(\Box^{\mathcal{A}}\psi).$$

(67)

This nesting operator is equivalent to the following expression highlighting the propagation direction of the STL variables:

$$\underset{\delta^{\rightarrow}}{\diamond}(\underset{\alpha^{\leftarrow}}{\Box^{\mathcal{A}}}\psi)\underset{\gamma}{\wedge}(\underset{\beta^{\rightarrow}}{\Box^{\mathcal{B}}}\varphi).$$

(68)

It is recalled that the naming conventions of STL variables follows the order of the Greek alphabet the more external or high in the tree the operator is. Here, the sign of $\delta_{N}$ respects the given trajectory.

To built a general formulation, about the propagation the following rules can be considered on its direction:

• •

  If interested in what happened before when the operator triggers, perform a forward propagation;

• •

  If interested in the future when the operator triggers, perform a backward propagation;

• •

  Bridges are not affected by propagation direction;

• •

  The last node is computed using a forward propagation in any case.