Smooth Robustness Measures for Symbolic Control Via Signal Temporal Logic

Smooth Robustness Measures for Symbolic Control Via Signal Temporal Logic

I Introduction

II Problem Formulation

III Smooth Robustness Measures (SRMs)

IV Approximation Errors of Smooth Robustness Measures

V The Gradients of Smooth Robustness Measures

VI Simulation Results

VII Conclusion

References

I Introduction

II Problem Formulation

III Smooth Robustness Measures (SRMs)

IV Approximation Errors of Smooth Robustness Measures

V The Gradients of Smooth Robustness Measures

VI Simulation Results

VII Conclusion

References

II-A STL Robust Semantics

II-B Synthesis Problem as an Optimization Problem

III-A SRM1: Proposed in [21]

III-B SRM2: Recovering the Soundness Property [20]

III-C SRM3: Recovering the reverse-soundness

III-D SRM4: Lifting the uniform robustness

IV-A Some Preliminaries

IV-B STL error semantics

V-A The gradient term: $\frac{\partial\tilde{\rho}^{\varphi}(s)}{\partial s}$

V-B The gradient term: $\frac{\partial s(u)}{\partial u}$

VI-A Effectiveness of the explicit gradients

VI-B Effectiveness of different SRMs

VI-C The use of approximation error bounds

II-A STL Robust Semantics

II-B Synthesis Problem as an Optimization Problem

III-A SRM1: Proposed in [21]

III-B SRM2: Recovering the Soundness Property [20]

III-C SRM3: Recovering the reverse-soundness

III-D SRM4: Lifting the uniform robustness

IV-A Some Preliminaries

IV-B STL error semantics

V-A The gradient term: ∂ρ~φ​(s)∂s\frac{\partial\tilde{\rho}^{\varphi}(s)}{\partial s}

V-B The gradient term: ∂s​(u)∂u\frac{\partial s(u)}{\partial u}

VI-A Effectiveness of the explicit gradients

VI-B Effectiveness of different SRMs

VI-C The use of approximation error bounds

V-A The gradient term: $\frac{\partial\tilde{\rho}^{\varphi}(s)}{\partial s}$

V-B The gradient term: $\frac{\partial s(u)}{\partial u}$

Notation

Semantic 1

Semantic 2

Semantic 3

Semantic 4

Semantic 5

Semantic 6

Notation

Semantic 1

Semantic 2

Semantic 3

Semantic 4

Semantic 5

Semantic 6

Abstract

Definition 1.

Remark 1.

Definition 2.

Lemma 1.

Proof.

Definition 3.

Lemma 2.

Proof.

Lemma 3.

Proof.

Lemma 4.

Proof.

Lemma 5.

Proof.

Lemma 6.

Proof.

Lemma 7.

Proof.

Remark 2.

Definition 4.

Theorem 1.

Proof.

Remark 3.

Definition 5.

Corollary 1.

Proof.

Definition 6.

Theorem 2.

Proof.

Lemma 8.

Proof.

Lemma 9.

Proof.

Theorem 3.

Proof.

Abstract

Definition 1.

Remark 1.

Definition 2.

Lemma 1.

Proof.

Definition 3.

Lemma 2.

Proof.

Lemma 3.

Proof.

Lemma 4.

Proof.

Lemma 5.

Proof.

Lemma 6.

Proof.

Lemma 7.

Proof.

Remark 2.

Definition 4.

Theorem 1.

Proof.

Remark 3.

Definition 5.

Corollary 1.

Proof.

Definition 6.

Theorem 2.

Proof.

Lemma 8.

Proof.

Lemma 9.

Proof.

Theorem 3.

Proof.

\useunder

\ul

Shirantha Welikala, Hai Lin and Panos J. Antsaklis The authors gratefully acknowledge the fruitful discussions with Vince Kurtz about different smooth robustness measures and their implementation.The support of the National Science Foundation (Grant No. IIS-1724070, CNS-1830335, IIS-2007949) is gratefully acknowledged.The authors are with the Department of Electrical Engineering, College of Engineering, University of Notre Dame, IN 46556, {wwelikal,hlin1,pantsakl}@bu.edu.

Symbolic control problems aim to synthesize control policies for dynamical systems under complex temporal specifications. For such problems, Signal Temporal Logic (STL) is increasingly used as the formal specification language due to its rich expressiveness. Moreover, the degree of satisfaction of STL specifications can be evaluated using STL robust semantics as a scalar robustness measure. This capability of STL enables transforming a symbolic control problem into an optimization problem that optimizes the corresponding robustness measure. However, since these robustness measures are non-smooth and non-convex, exact solutions can only be computed using computationally inefficient mixed-integer programming techniques that do not scale well. Therefore, recent literature has focused on using smooth approximations of these robustness measures to apply scalable and computationally efficient gradient-based methods to find local optima solutions. In this paper, we first generalize two recently established smooth robustness measures (SRMs) and two new ones and discuss their strengths and weaknesses. Next, we propose STL error semantics to characterize the approximation errors associated with different SRMs under different parameter configurations. This allows one to sensibly select an SRM (to optimize) along with its parameter values. We then propose STL gradient semantics to derive explicit gradients of SRMs leading to improve computational efficiency as well as accuracy compared to when using numerically estimated gradients. Finally, these contributions are highlighted using extensive simulation results.

A symbolic control problem arises when a dynamical system needs to be controlled such that its trajectory satisfies some complex temporal specifications. For example, such specifications may include requirements expected from the dynamical system, like achieving time-sensitive goals, avoiding undesirable behaviors and ensuring desirable behaviors over certain periods of time. To precisely express such temporal specifications, temporal logics like Linear Temporal Logic [1], Computation Tree Logic [2], Interval Temporal Logic [3], Metric Temporal logic [4], Time Window Temporal Logic [5] and Signal Temporal Logic (STL) [6] can be used.

Among these temporal logics, STL has the advantage of having STL robust semantics that can systematically transform the given temporal specifications and a system trajectory (i.e., a “signal”) into a scalar robustness measure - which is indicative of both the satisfaction/violation and the degree of satisfaction/violation of the specification via its sign and magnitude, respectively. This unique property enables STL to transform a symbolic control problem into an optimization problem that finds the control sequence (signal) that maximizes the corresponding robustness measure. Due to these capabilities of STL, in recent years, it has been increasingly used in control systems related application domains such as in planning [7], robotics [8], multi-agent systems [9], automotive systems [10], cyber-physical systems [11] and biological systems [12, 13].

The conventional robustness measure is non-smooth and non-convex due to the involved min and max operators in its definition. Therefore, optimizing such a robustness measure is an extremely challenging task. The work in [14] formulates this optimization problem as a Mixed-Integer Program (MIP) so as to obtain an exact solution. However, this MIP formulation scales poorly with respect to many aspects of the original optimization problem (e.g., the complexity of the specification). Moreover, MIPs are inherently computationally inefficient to solve due to their complexity properties. With regard to this optimization problem, prior work have also explored alternative MIP formulations [15, 11] as well as heuristic [16, 17] and non-smooth [18, 19] optimization approaches, but with no solution to the aforementioned scalability and computational efficiency concerns.

To address these concerns, several recent works such as [7, 8, 20] pioneered by [21] propose to use smooth approximations of the conventional robustness measure so as to exploit the scalable, computationally efficient and well-established gradient-based optimization methods. It is worth noting that even though gradient-based optimization methods are susceptible to the issue of local optima, there are several efficient and practical ways to overcome this issue [22, 23, 24]. Moreover, the consensus in the literature [21, 9, 7, 8, 20] seems to indicate that the scalability and the computational efficiency offered by adopting gradient-based optimization methods outweigh the effect of any such drawbacks.

Typically, an approximate smooth robustness measure (SRM) is obtained by replacing (approximating) the min and max operators in the conventional robustness measure with some smooth operators. Therefore, depending on the nature of the used smooth operators, the resulting SRM will have different characteristics. For example, [21] proposes to use quasi-min and quasi-max [25] operators as the smooth operators. However, even though the resulting SRM is globally smooth, it is not sound, i.e., achieving a positive value for the SRM does not imply the satisfaction of the specification [21]. To recover this soundness property, [7] proposes to use smooth operators based on arithmetic and geometric means (partly motivated by [8]). Even though the resulting SRM ensures soundness and also leads to more conservative results (i.e., more uniformly robust to external disturbances), it is not globally smooth [7]. Motivated by this predicament, the subsequent work [20] (which also is the predecessor to this work) proposes to use quasi-min and soft-max [25] operators as smooth operators. The resulting SRM is sound, globally smooth, and also offers a tunable level of conservativeness [20] (via selecting the parameters of the used smooth operators).

Despite these successive recent improvements, there still are many contributions to be made in this research. For example, even though the proposed SRMs in [7] and [20] are sound, they are not reverse sound, i.e., achieving a negative value for the SRM does not imply the violation of the specification. In fact, in some applications (e.g., in falsification problems [16]), the reverse soundness property is far more crucial than the soundness property. To address this need, inspired by [21, 20], in this paper, we propose a new SRM that is reverse sound and also globally smooth. Along the same lines, we propose another SRM that aims to provide more flexibility when tuning the level of conservativeness (still, via selecting the parameters of the used smooth operators).

A natural question to ask at this point is: “How one should select these smooth operator parameters?” Typically, smaller parameter values lead to more conservative results, while larger parameter values lead to more accurate SRM (i.e., closer to the actual robustness measure). Authors in [21] motivate the latter accuracy argument as it leads to ensure properties like soundness and reverse soundness (together called completeness) asymptotically. However, authors in [20] point out the prior conservativeness argument. Nevertheless, both works do not provide a systematic approach to select these parameters. To answer this question, in this paper, we propose STL error semantics to determine a bound for the approximation error associated with the used SRM in terms of the used operator parameters. Note that, since the width of such an error bound is a measure of the accuracy of the used SRM in terms of the used operator parameters, it can easily be used to tune the operator parameters and compare different (existing and newly proposed) SRMs.

As mentioned before, the primary motivation behind using an SRM (as opposed to using the non-smooth conventional robustness measure) is to enable the use of efficient and scalable gradient-based optimization methods [21, 9, 8, 7, 20]. Therefore, intuitively, to best reap these benefits of gradient-based optimization, having an accurate as well as efficient way to evaluate the required “gradients” is of prime importance (here, the “gradients” refer to the gradients of the used SRM with respect to the system controls). Clearly, the use of numerically evaluated gradients is both computationally inefficient as well as inaccurate [21]. However, to the best of the authors’ knowledge, experimental results reported in existing literature [21, 9, 8, 7, 20] use numerically evaluated gradients defined via finite differences [21] or software packages like AutoGrad [26]. Motivated by this, we propose STL gradient semantics to determine the explicit gradient of any used SRM. Such derived explicit gradients are accurate (by definition) and significantly efficient compared to numerically evaluated gradients, and thus, allows us to reap the benefits of gradient-based optimization methods to the fullest.

In all, our contributions can be summarized as follows:

1.

Two new SRMs are proposed. One is guaranteed to be reverse sound, while the other is intended to provide more flexibility when tuning the level of conservativeness.
2.

We propose STL error semantics to determine a bound for the approximation error of the used SRM in terms of the used operator parameters, enabling one to sensibly select an SRM along with its smooth parameter values.
3.

We propose STL gradient semantics to derive the explicit gradient of the used SRM, leading to improve the accuracy and the efficiency (of both gradients and results) compared to when using numerically estimated gradients.
4.

An extensive collection of simulation results has been reported along with source codes for reproduction and reuse purposes.

This paper is organized as follows. Section II introduces the considered class of symbolic control problems and the STL robust semantics. Section III provides the details of existing and new SRMs and introduces the smooth STL robust semantics. The proposed STL error semantics that can be used to characterize the approximation errors associated with different SRMs are discussed in Section IV. The proposed STL gradient semantics that can be used to derive explicit gradients of SRMs are discussed in Section V. Several observed simulation results, along with few interesting future research directions, are provided in Section VI before concluding the paper in Section VII.

We consider a non-linear discrete-time system of the form:

	$\displaystyle x_{t+1}=$	$\displaystyle f(x_{t},u_{t}),$		(1)
	$\displaystyle y_{t}=$	$\displaystyle g(x_{t},u_{t}),$		(1)

where $x_{t}\in\mathcal{X}\subseteq\mathbb{R}^{n}$ is the system state, $u_{t}\in\mathcal{U}\subseteq\mathbb{R}^{m}$ is the control input, and $y_{t}\in\mathcal{Y}\subseteq\mathbb{R}^{p}$ is the output signal. It is also assumed that $f(\cdot,\cdot)$ and $g(\cdot,\cdot)$ in (1) are continuous and differentiable. Given a finite horizon $T$ , an initial condition $x_{0}$ and a bounded-time STL specification $\varphi_{0}$ , our goal is to synthesize a control input sequence $u\triangleq\{u_{t}\}_{t\in[0,T]}$ such that the resulting output signal $y\triangleq\{y_{t}\}_{t\in[0,T]}$ satisfies $\varphi_{0}$ (here, $[0,T]$ denotes the discrete interval $\{0,1,2,\ldots,T\}$ ).

STL was first introduced in [6] as a variant of temporal logic tailored for specifying desired temporal properties of real-valued signals. In particular, an STL specification $\varphi$ is built recursively from the predicates using the STL syntax:

\varphi:=\pi|\neg\varphi|\varphi_{1}\land\varphi_{2}|\varphi_{1}\mathbf{U}_{[t_{1},t_{2}]}\varphi_{2},

(2)

where $\pi=(\mu^{\pi}(y_{t})\geq 0)$ is a predicate defined by the function $\mu^{\pi}:\mathbb{R}^{p}\rightarrow\mathbb{R}$ . While some STL synthesis methods require $\mu^{\pi}(\cdot)$ to be linear, in our approach, we only require $\mu^{\pi}(\cdot)$ to be differentiable. The conjunction ( $\land$ ) and negation ( $\neg$ ) operators can be used to derive other Boolean operators such as disjunction ( $\lor$ ) and implication ( $\implies$ ). Similarly, the until ( $\varphi_{1}\mathbf{U}_{[t_{1},t_{2}]}\varphi_{2}$ ) operator can be used to derive other temporal operators such as eventually ( $\mathbf{F}_{[t_{1},t_{2}]}\varphi$ ) and always ( $\mathbf{G}_{[t_{1},t_{2}]}\varphi$ ). Here $[t_{1},t_{2}]$ represents a discrete interval starting from a time point $t_{1}$ to a time point $t_{2}\geq t_{1}$ where $t_{1},t_{2}\in\mathbb{Z}$ . Since we restrict ourselves to bounded-time STL specifications, $t_{2}<\infty$ .

For example, the STL specification $\varphi=(\textbf{G}_{[a,b]}\varphi_{1})\land(\textbf{F}_{[b,c]}\varphi_{2})$ states that “ $\varphi_{1}$ must be True at all time points in $[a,b]$ and $\varphi_{2}$ must be True at some time point in $[b,c]$ .” Here, each $\varphi_{i},i\in\{1,2\}$ is an STL specification itself, which incidentally can be a predicate $\varphi_{i}=\pi_{i}=(\mu^{\pi_{i}}(y_{t})\geq 0)$ . In the latter case, notice the dependence of $\varphi_{i}$ on the time point $t\in[0,T]\supseteq[a,c]$ .

We use the STL robust semantics (defined below) to assign a scalar value (called the robustness measure) for a signal with respect to a given specification. This particular robustness measure is positive if and only if the signal satisfies the given specification. In other words, $\rho^{\varphi}(y)>0\iff y\vDash\varphi$ , where $\rho^{\varphi}(y)$ is the robustness measure of the signal $y$ with respect to the specification $\varphi$ . Let us use the notation $(y,t)\triangleq\{y_{\tau}\}_{\tau\in[t,T]}$ to denote the suffix of the signal $y(\triangleq\{y_{\tau}\}_{\tau\in[0,T]})$ starting from time point $t$ (note that, $y\equiv(y,0)$ ).

(STL Robust Semantics)

•

$y\vDash\varphi\iff\rho^{\varphi}((y,0))>0$
•

$y\nvDash\varphi\iff\rho^{\varphi}((y,0))<0$
•

$\rho^{\pi}((y,t))=\mu^{\pi}(y_{t})$
•

$\rho^{\neg\varphi}((y,t))=-\rho^{\varphi}((y,t))$
•

$\rho^{\varphi_{1}\land\varphi_{2}}((y,t))=\min\{\rho^{\varphi_{1}}((y,t)),\,\rho^{\varphi_{2}}((y,t))\}$
•

$\rho^{\varphi_{1}\lor\varphi_{2}}((y,t))=\max\{\rho^{\varphi_{1}}((y,t)),\,\rho^{\varphi_{2}}((y,t))\}$
•

$\rho^{\mathbf{F}_{[t_{1},t_{2}]}\varphi}((y,t))=\max_{\tau\in[t+t_{1},t+t_{2}]}\{\rho^{\varphi}((y,\tau))\}$
•

$\rho^{\mathbf{G}_{[t_{1},t_{2}]}\varphi}((y,t))=\min_{\tau\in[t+t_{1},t+t_{2}]}\{\rho^{\varphi}((y,\tau))\}$
•

$\rho^{\varphi_{1}\mathbf{U}_{[t_{1},t_{2}]}\varphi_{2}}((y,t))=\max_{\tau\in[t+t_{1},t+t_{2}]}\{\min\{$
$\rho^{\varphi_{1}}((y,\tau)),\min_{\delta\in[t+t_{1},\tau]}\{\rho^{\varphi_{2}}((y,\delta))\}\}$

Finding a control input sequence $u$ for the system (1) so that the resulting output signal $y$ satisfies the given specification $\varphi_{0}$ is formally known as the synthesis problem. Using STL robust semantics discussed above, this synthesis problem can be stated as an optimization problem of the form:

Note that the three feasibility constraints in the last line of (3) can be included in the robustness measure (i.e., in the objective function of (3)) by considering them as STL specifications, say $\varphi_{y},\varphi_{x},\varphi_{u}$ , on respective signals $y,x,u$ (similar to $y$ and $u$ , $x\triangleq\{x_{t}\}_{t\in[0,T]}\equiv(x,0)$ ). For example, if $\mathcal{U}=\{u:u\in\mathbb{R}^{m},\|u\|\leq a\}$ , then, $\varphi_{u}=\textbf{G}_{[0,T]}(a-\|u_{t}\|\geq 0)$ .

Therefore, (3) can be re-stated as

$\displaystyle u^{*}=$	$\displaystyle\ \underset{u}{\arg\max}$	$\displaystyle\rho^{\varphi}(y,x,u)$	(4)
	Subject to:	$\displaystyle x_{t+1}=f(x_{t},u_{t}),\ x_{0}\mbox{ is a given,}$
	$\displaystyle y_{t}=g(x_{t},u_{t}),\ \forall t\in[0,T],$

where $\varphi\triangleq\varphi_{0}\land\varphi_{y}\land\varphi_{x}\land\varphi_{u}$ , and hence, $\rho^{\varphi}(y,x,u)=\max\{\rho^{\varphi_{0}}(y),\,\rho^{\varphi_{y}}(y),\,\rho^{\varphi_{x}}(x),\,\rho^{\varphi_{u}}(u)\}$ . With a slight abuse of notation, we can replace the STL specification $\varphi_{0}\land\varphi_{y}$ simply by $\varphi_{y}$ . As a result, the robustness measure objective in (4) can be written of as

\rho^{\varphi}(y,x,u)\triangleq\max\{\rho^{\varphi_{y}}(y),\,\rho^{\varphi_{x}}(x),\,\rho^{\varphi_{u}}(u)\}.

(5)

It is worth pointing out that the state signal $x$ and the output signal $y$ are both fully determined by the control signal $u$ through the agent dynamics (1) and the given initial condition $x_{0}$ . Exploiting this dependence, we can define a composite control dependent signal $s(u)\triangleq\{s_{t}(u)\}_{t\in[0,T]}$ where $s_{t}(u)\triangleq[y_{t}^{\top}(u),x_{t}^{\top}(u),u_{t}^{\top}]^{\top}\in\mathbb{R}^{p+n+m}$ . Hence, $\rho^{\varphi}(y,x,u)$ in (5) can be written as $\rho^{\varphi}(s(u))=\rho^{\varphi}(y(u),x(u),u)$ . Therefore, (4) can be re-stated as an unconstrained optimization problem:

u^{*}=\underset{u}{\arg\max}\ \rho^{\varphi}(s(u)),

(6)

where the objective function $\rho^{\varphi}(s(u))$ is simply the robustness measure of the signal $s(u)$ with respect to the specification $\varphi$ .

According to the STL robust semantics, if the determined optimal control signal $u^{*}$ in (6) is such that $\rho^{\varphi}(s(u^{*}))>0$ , the signal $s(u^{*})$ is guaranteed to satisfy the specification $\varphi$ . In other words, denoting the corresponding output and state signals respectively as $y^{*}$ and $x^{*}$ , $y^{*}$ is guaranteed to satisfy the given specification $\varphi_{0}$ in (3), and, signals $y^{*}$ , $x^{*}$ and $u^{*}$ will always remain within their respective feasible regions stated in (3).

In this paper, we focus on solving the optimization problem (6) (same as (3) and (4)) to determine the optimal controls for the synthesis problem. An alternative energy-aware approach would be to solve an optimization problem of the form

u^{*}=\underset{u}{\arg\max}\ \rho^{\varphi}(s(u))-\alpha\|u\|^{2},

(7)

where $\alpha\in\mathbb{R}$ is a scaling factor. Similarly, an alternative receding horizon control approach (preferred if $T$ is large) can also be facilitated - by slightly modifying the form of (7).

The robustness measure objective $\rho^{\varphi}(s(u))$ of the optimization problem (6) (i.e., the interested synthesis problem) is non-smooth and non-convex due to the involved non-smooth $\min\{\cdot\}$ and $\max\{\cdot\}$ operators in the STL robust semantics. In the special case where the system (1) is linear and all the predicates required to define the STL specification $\varphi$ are linear, the problem (6) can be encoded as a Mixed Integer Program (MIP) [14]. However, the complexity of this MIP’s solution process grows exponentially with the number of predicates and $T$ . Therefore, even for such a special (linear) case, solving (6) is extremely challenging.

To address this challenge, the recent literature [21, 8, 7, 20] has focused on replacing the non-smooth robustness measure objective $\rho^{\varphi}(s(u))$ in (6) with a smooth approximation of it. Such a smooth approximation is denoted as $\tilde{\rho}^{\varphi}(s(u))$ and is referred to as a smooth robustness measure (SRM). This modification enables the use of computationally efficient and scalable gradient-based optimization techniques to solve (6).

Typically, an SRM $\tilde{\rho}^{\varphi}(s(u))$ is obtained by replacing (approximating) the non-smooth $\min\{\cdot\}$ and $\max\{\cdot\}$ operators involved in $\rho^{\varphi}(s(u))$ by respective smooth-min and smooth-max operators (denoted as $\widetilde{\min}\{\cdot\}$ and $\widetilde{\max}\{\cdot\}$ ). In particular, to evaluate such an SRM $\tilde{\rho}^{\varphi}(s(u))$ , we use the smooth STL robust semantics defined below.

(Smooth STL Robust Semantics)

•

$\tilde{\rho}^{\pi}((s,t))=\mu^{\pi}(s_{t})$
•

$\tilde{\rho}^{\neg\pi}((s,t))=-\tilde{\rho}^{\pi}((s,t))$
•

$\tilde{\rho}^{\varphi_{1}\land\varphi_{2}}((s,t))=\widetilde{\min}\{\tilde{\rho}^{\varphi_{1}}((s,t)),\,\tilde{\rho}^{\varphi_{2}}((s,t))\}$
•

$\tilde{\rho}^{\varphi_{1}\lor\varphi_{2}}((s,t))=\widetilde{\max}\{\tilde{\rho}^{\varphi_{1}}((s,t)),\,\tilde{\rho}^{\varphi_{2}}((s,t))\}$
•

$\tilde{\rho}^{\mathbf{F}_{[t_{1},t_{2}]}\varphi}((s,t))=\widetilde{\max}_{\tau\in[t+t_{1},t+t_{2}]}\{\tilde{\rho}^{\varphi}((s,\tau))\}$
•

$\tilde{\rho}^{\mathbf{G}_{[t_{1},t_{2}]}\varphi}((s,t))=\widetilde{\min}_{\tau\in[t+t_{1},t+t_{2}]}\{\tilde{\rho}^{\varphi}((s,\tau))\}$
•

$\tilde{\rho}^{\varphi_{1}\mathbf{U}_{[t_{1},t_{2}]}\varphi_{2}}((s,t))=\widetilde{\max}_{\tau\in[t+t_{1},t+t_{2}]}\{\widetilde{\min}\{\newline \tilde{\rho}^{\varphi_{1}}((s,\tau)),\,\widetilde{\min}_{\delta\in[t+t_{1},\tau]}\{\tilde{\rho}^{\varphi_{2}}((s,\delta))\}\}\}$

In writing the above semantics, for notational simplicity, we have omitted representing the control ( $u$ ) dependence of the composite signal ( $s(u)$ ). Moreover, without loss of generality, we have assumed that the STL specification is given in disjunctive normal form, i.e., the negation operator is only applied to predicates $\pi$ . It is worth noting that any STL specification can be written in disjunctive normal form [20].

TABLE I: A summary of available different smooth-min (

\widetilde{\min}\{\cdot\}

) and smooth-max (

\widetilde{\max}\{\cdot\}

) operators and their characteristics. Here,

a\triangleq\{a_{1},a_{2},\ldots,a_{m}\}

is a finite set of real numbers (assume to be in descending order) and parameters

k_{1},k_{2}\in\mathbb{R}_{>0}

Smooth Operator

Operator Definition

Gradient

(e.g.,

\frac{\partial}{\partial a_{i}}\widetilde{\min}\{a\}=\,?

)

Approximation Error Band

(e.g.,

(\min\{a\}-\widetilde{\min}\{a\})\in\,?

)

k_{1}

-Quasi-

\min

\widetilde{\min}\{a\}\triangleq-\frac{1}{k_{1}}\log\left(\sum_{i=1}^{m}e^{-k_{1}a_{i}}\right)

\frac{e^{-k_{1}a_{i}}}{\sum_{j=1}^{m}e^{-k_{1}a_{j}}}

[0,\ \frac{\log(m)}{k_{1}}]

k_{2}

-Quasi-

\max

\widetilde{\max}\{a\}\triangleq\frac{1}{k_{2}}\log\left(\sum_{i=1}^{m}e^{k_{2}a_{i}}\right)

\frac{e^{k_{2}a_{i}}}{\sum_{j=1}^{m}e^{k_{2}a_{j}}}

[-\frac{\log(m)}{k_{2}},\ 0]

k_{1}

-Soft-

\min

\widetilde{\min}\{a\}\triangleq\frac{\sum_{i=1}^{m}a_{i}e^{-k_{1}a_{i}}}{\sum_{i=1}^{m}e^{-k_{1}a_{i}}}

\frac{e^{-k_{1}a_{i}}}{\sum_{j=1}^{m}e^{-k_{1}a_{j}}}\left[1-k_{1}(a_{i}-\widetilde{\min}\{\bar{a}\})\right]

[-\frac{a_{1}-a_{m}}{1+\frac{e^{k_{1}(a_{m-1}-a_{m})}}{m-1}},\ 0]

k_{2}

-Soft-

\max

\widetilde{\max}\{a\}\triangleq\frac{\sum_{i=1}^{m}a_{i}e^{k_{2}a_{i}}}{\sum_{i=1}^{m}e^{k_{2}a_{i}}}

\frac{e^{k_{2}a_{i}}}{\sum_{j=1}^{m}e^{k_{2}a_{j}}}\left[1-k_{2}(\widetilde{\max}\{\bar{a}\}-a_{i})\right]

[0,\ \frac{a_{1}-a_{m}}{1+\frac{e^{k_{2}(a_{1}-a_{2})}}{m-1}}]

TABLE II: Different smooth robustness measures (SRMs) defined by the used smooth-min and smooth-max operators.

SRM Type

Smooth-max

Operator

k_{2}

-Quasi-

\max

k_{2}

-Soft-

\max

Smooth-min Operator

k_{1}

-Quasi-

\min

SRM1

(Proposed in [21])

SRM2

(Proposed in [20])

k_{1}

-Soft-

\min

SRM3

(New)

SRM4

(New)

Table I summarizes possible two smooth-min operators and two smooth-max operators that can be used in Def. 2. Based on the configuration of the used smooth-min and smooth-max operators, as outlined Tab. II, we can define four different SRMs (labeled SRM1-4). In the following four subsections, we discuss each of these different SRMs.

Unless stated otherwise, $a\triangleq\{a_{1},a_{2},\ldots,a_{m}\}$ is used to represent an arbitrary finite set of real numbers (without loss of generality, $a$ is also assumed to be in descending order). Further, $k_{1},k_{2}\in\mathbb{R}_{>0}$ are used to represent two user defined parameters. We also point out that, we have slightly abused the notation $[\cdot,\cdot]$ by using it to represent closed intervals in both $\mathbb{R}$ and $\mathbb{Z}$ . However, we believe its meaning would be clear from the context.

The work in [21] has proposed to use $k_{1}$ -Quasi- $\min$ and $k_{2}$ -Quasi- $\max$ operators (see Tab. I and [25]):

	$\displaystyle\widetilde{\min}\{a\}\triangleq$	$\displaystyle-\frac{1}{k_{1}}\log\left(\sum_{i=1}^{m}e^{-k_{1}a_{i}}\right)\mbox{ and }$		(8)
	$\displaystyle\widetilde{\max}\{a\}\triangleq$	$\displaystyle\ \ \ \ \frac{1}{k_{2}}\log\left(\sum_{i=1}^{m}e^{k_{2}a_{i}}\right),$		(8)

as smooth-min and smooth-max operators, respectively. The operators in (8) are smooth everywhere, and thus, their respective gradients can be derived easily (provided in Tab. I). The following lemma establishes bounds on the approximation errors associated with the operators in (8).

The smooth-min and smooth-max operators in (8) satisfy the following respective approximation error bounds:

$\displaystyle(\min\{a\}-\widetilde{\min}\{a\})\in$	$\displaystyle[0,\,\frac{1}{k_{1}}\log(1+(m-1)e^{-k_{1}(a_{m-1}-a_{m})})]$	(9)
$\displaystyle\subseteq$	$\displaystyle[0,\ \frac{\log(m)}{k_{1}}]\mbox{ and }$
$\displaystyle(\max\{a\}-\widetilde{\max}\{a\})\in$	$\displaystyle[-\frac{1}{k_{2}}\log(1+(m-1)e^{-k_{2}(a_{1}-a_{2})}),\,0]$
$\displaystyle\subseteq$	$\displaystyle[-\frac{\log(m)}{k_{2}},\ 0].$

Recall that the set $a=\{a_{1},a_{2},\ldots,a_{m}\}$ is in descending order. Therefore, the approximation error associated with the smooth-min operator in (8) is

$\displaystyle(\min\{a\}-$	$\displaystyle\widetilde{\min}\{a\})=\ a_{m}+\frac{1}{k_{1}}\log\left(\sum_{i=1}^{m}e^{-k_{1}a_{i}}\right)$
$\displaystyle=$	$\displaystyle\frac{1}{k_{1}}\log\left(\frac{\sum_{i=1}^{m}e^{-k_{1}a_{i}}}{e^{-k_{1}a_{m}}}\right)$
$\displaystyle=$	$\displaystyle\frac{1}{k_{1}}\log\left(1+\frac{\sum_{i=1}^{m-1}e^{-k_{1}a_{i}}}{e^{-k_{1}a_{m}}}\right)$
$\displaystyle\leq$	$\displaystyle\frac{1}{k_{1}}\log\left(1+\frac{\sum_{i=1}^{m-1}e^{-k_{1}a_{m-1}}}{e^{-k_{1}a_{m}}}\right)$
$\displaystyle=$	$\displaystyle\frac{1}{k_{1}}\log\left(1+(m-1)e^{-k_{1}(a_{m-1}-a_{m})}\right)$	(10)
$\displaystyle\leq$	$\displaystyle\ \frac{\log(m)}{k_{1}}.$	(11)

Both inequalities used in the above derivation exploit the monotonicity property of the $\log(\cdot)$ function. Using the same property, we can also write

$\displaystyle(\min\{a\}-\widetilde{\min}\{a\})=$	$\displaystyle\ a_{m}+\frac{1}{k_{1}}\log\left(\sum_{i=1}^{m}e^{-k_{1}a_{i}}\right)$
$\displaystyle\geq$	$\displaystyle\ a_{m}+\frac{1}{k_{1}}\log\left(e^{-k_{1}a_{m}}\right)$
$\displaystyle=$	$\displaystyle\ 0.$	(12)

The relationships in (10), (11) and (12) establish the first result in (9). Following the same steps, the second result in (9) can also be established. This completes the proof. ∎

From the above lemma, it is clear that the approximation errors associated with the smooth-min and smooth-max operators in (8) are bounded and also vanishes as $k_{1},k_{2}\rightarrow\infty$ . Since these operators are used when determining the SRM1 $\tilde{\rho}^{\varphi}(s(u))$ (via Def. 2), we can use (9) to bound the approximation error associated with the SRM1 as

(\rho^{\varphi}(s(u))-\tilde{\rho}^{\varphi}(s(u))\in[L_{k}^{\varphi},U_{k}^{\varphi}],

(13)

where $L_{k}^{\varphi}$ and $U_{k}^{\varphi}$ are two real numbers dependent on the STL specification $\varphi$ and the parameters $k=[k_{1},k_{2}]$ . In other words, the actual (non-smooth) robustness measure $\rho^{\varphi}(s(u))$ with respect to the SRM1 $\tilde{\rho}^{\varphi}(s(u))$ is placed such that

\tilde{\rho}^{\varphi}(s(u))+L_{k}^{\varphi}\leq\rho^{\varphi}(y,x,u)\leq\tilde{\rho}^{\varphi}(s(u))+U_{k}^{\varphi}.

(14)

The exact details on how $L_{k}^{\varphi}$ and $U_{k}^{\varphi}$ can be computed are provided in Section IV. Regardless, at this point, it should be clear from (9) that neither $L_{k}^{\varphi}$ nor $U_{k}^{\varphi}$ in (13) is necessarily zero. This implies that, in this scenario (SRM1), achieving $\tilde{\rho}^{\varphi}(s(u))>0$ for some composite signal $s(u)$ does not guarantee the satisfaction of the specification $\varphi$ , i.e.,

\tilde{\rho}^{\varphi}(s(u))>0\centernot\implies\rho^{\varphi}(s(u))>0.

Similarly, in this scenario (SRM1), achieving $\tilde{\rho}^{\varphi}(s(u))<0$ for some composite signal $s(u)$ does not guarantee the violation of the specification $\varphi$ either, i.e.,

\tilde{\rho}^{\varphi}(s(u))<0\centernot\implies\rho^{\varphi}(s(u))<0.

The above two characteristics indicate that the SRM1 is neither sound, revers-soundness nor complete. The formal definitions of these concepts: soundness, reverse-soundness and completeness considered in this paper are given in the following definition.

A smooth robustness measure $\tilde{\rho}^{\varphi}(\cdot)$ is called:

1.

“sound” if $\tilde{\rho}^{\varphi}(s(u))>0\implies\rho^{\varphi}(s(u))>0$ , for any signal $s(u)$ and specification $\varphi$ ,
2.

“reverse-sound” if $\tilde{\rho}^{\varphi}(s(u))<0\implies\rho^{\varphi}(s(u))<0$ , for any signal $s(u)$ and specification $\varphi$ ,
3.

“complete” if it is both sound and reverse-sound.

Since the approximation errors associated with the smooth-min and smooth-max operators in (8) vanish as the parameters $k_{1},k_{2}\rightarrow\infty$ (see Lm. 1), the same can be expected from the approximation error associated with the SRM1, i.e., as $k_{1},k_{2}\rightarrow\infty$ , the SRM1 $\tilde{\rho}^{\varphi}(s(u))\rightarrow\rho^{\varphi}(s(u))$ . Therefore, as $k_{1},k_{2}\rightarrow\infty$ , SRM1 becomes sound, reverse-sound and complete. Hence, the SRM1 is called asymptotically sound, asymptotically reverse-sound and asymptotically complete.

Even though the aforementioned asymptotic properties of SRM1 are theoretically reassuring, when it comes to implementations, allowing the parameters $k_{1},k_{2}\rightarrow\infty$ is not practical (see (8)). This limitation is partially addressed in [20] by proposing a new SRM (labeled as SRM2) that is sound - irrespective of the parameters $k_{1},k_{2}\in\mathbb{R}_{>0}$ . Moreover, this SRM2 is asymptotically reversed-sound and asymptotically complete. In all, SRM2 [20] recovers the lacking soundness property in SRM1 [21].

In particular, SRM2 is defined using $k_{1}$ -Quasi- $\min$ and $k_{2}$ -Soft- $\max$ operators (see Tab. I):

	$\displaystyle\widetilde{\min}\{a\}=$	$\displaystyle-\frac{1}{k_{1}}\log\left(\sum_{i=1}^{m}e^{-k_{1}a_{i}}\right)\mbox{ and}$		(15)
	$\displaystyle\widetilde{\max}\{a\}=$	$\displaystyle\frac{\sum_{i=1}^{m}a_{i}e^{k_{2}a_{i}}}{\sum_{i=1}^{m}e^{k_{2}a_{i}}},$		(15)

as smooth-min and smooth-max operators, respectively. Similar to before, the above operators are smooth everywhere, and their respective gradients are provided in Tab I. The following lemma establishes the bounds on the approximation errors associated with the operators in (15).

The smooth-min and smooth-max operators in (15) satisfy the following respective approximation error bounds:

$\displaystyle(\min\{a\}-\widetilde{\min}\{a\})\in$	$\displaystyle[0,\,\frac{1}{k_{1}}\log(1+(m-1)e^{-k_{1}(a_{m-1}-a_{m})})]$	(16)
$\displaystyle\subseteq$	$\displaystyle[0,\,\frac{\log(m)}{k_{1}}]\mbox{ and }$
$\displaystyle(\max\{a\}-\widetilde{\max}\{a\})\in$	$\displaystyle[0,\,(a_{1}-a_{m})(1-\frac{1}{\sum_{i=1}^{m}e^{-k_{2}(a_{1}-a_{i})}})]$
$\displaystyle\subseteq$	$\displaystyle[0,\,\frac{a_{1}-a_{m}}{1+\frac{e^{k_{2}(a_{1}-a_{2})}}{m-1}}].$

The first result in (16) has already been proven in Lm. 1. Hence, here we only need to prove the second result in (16). The approximation error associated with the smooth-max operator in (15) is

$\displaystyle(\max\{a\}-$	$\displaystyle\widetilde{\max}\{a\})=a_{1}-\frac{\sum_{i=1}^{m}a_{i}e^{k_{2}a_{i}}}{\sum_{i=1}^{m}e^{k_{2}a_{i}}}$
$\displaystyle=$	$\displaystyle\frac{a_{1}\sum_{i=2}^{m}e^{k_{2}a_{i}}-\sum_{i=2}^{m}a_{i}e^{k_{2}a_{i}}}{\sum_{i=1}^{m}e^{k_{2}a_{i}}}$
$\displaystyle\leq$	$\displaystyle\frac{a_{1}\sum_{i=2}^{m}e^{k_{2}a_{i}}-a_{m}\sum_{i=2}^{m}e^{k_{2}a_{i}}}{\sum_{i=1}^{m}e^{k_{2}a_{i}}}$
$\displaystyle=$	$\displaystyle(a_{1}-a_{m})\frac{\sum_{i=2}^{m}e^{k_{2}a_{i}}}{\sum_{i=1}^{m}e^{k_{2}a_{i}}}$	(17)
$\displaystyle=$	$\displaystyle(a_{1}-a_{m})\left(1-\frac{1}{\sum_{i=1}^{m}e^{-k_{2}(a_{1}-a_{i})}}\right).$	(18)

An alternative lower bound can be obtained by continuing from (17) as

	$\displaystyle(\max\{a\}-\widetilde{\max}\{a\})\leq$	$\displaystyle\frac{(a_{1}-a_{m})}{\frac{\sum_{i=1}^{m}e^{k_{2}a_{i}}}{\sum_{i=2}^{m}e^{k_{2}a_{i}}}}=\frac{(a_{1}-a_{m})}{1+\frac{e^{k_{2}a_{1}}}{\sum_{i=2}^{m}e^{k_{2}a_{i}}}}$
	$\displaystyle\leq$	$\displaystyle\frac{(a_{1}-a_{m})}{1+\frac{e^{k_{2}(a_{1}-a_{2})}}{m-1}}.$		(19)

All the inequalities used in the above derivations exploit the monotonicity property the exponential function. Using the same property, we can also write

$\displaystyle(\max\{a\}-\widetilde{\max}\{a\})=$	$\displaystyle\ a_{1}-\frac{\sum_{i=1}^{m}a_{i}e^{k_{2}a_{i}}}{\sum_{i=1}^{m}e^{k_{2}a_{i}}}$
$\displaystyle\geq$	$\displaystyle\ a_{1}-\frac{a_{1}\sum_{i=1}^{m}e^{k_{2}a_{i}}}{\sum_{i=1}^{m}e^{k_{2}a_{i}}}$
$\displaystyle=$	$\displaystyle\ 0.$	(20)

The relationships in (18), (19) and (20) prove the second result in (16), and thus, the proof is complete. ∎

Recall that the operators in (15) define the SRM2 $\tilde{\rho}^{\varphi}(s(u))$ via Def. 2. Now, the following lemma can be established regarding the approximation error associated with the SRM2.

The approximation error associated with the SRM2 $\tilde{\rho}^{\varphi}(s(u))$ is bounded such that

(\rho^{\varphi}(s(u))-\tilde{\rho}^{\varphi}(s(u)))\in[0,U_{k}^{\varphi}],

(21)

where $U_{k}^{\varphi}$ is some positive real number dependent on the specification $\varphi$ and the parameters $k=[k_{1},k_{2}]$ , and $U_{k}^{\varphi}\rightarrow 0$ as $k_{1},k_{2}\rightarrow\infty$ .

Lemma 2 implies that for any set of real numbers $a$ , the smooth operators in (15) satisfy $\widetilde{\min}\{a\}\leq\min\{a\}$ and $\widetilde{\max}\{a\}\leq\max\{a\}$ . Note also that SRM2 $\tilde{\rho}^{\varphi}(s(u))$ is computed recursively using the semantics in Def. 2 while $\rho^{\varphi}(s(u))$ is computed recursively using the semantics in Def. 1. Then, from comparing the respective semantics in Defs. 1 and 2, it is easy to see that $\tilde{\rho}^{\varphi}(s(u))\leq\rho^{\varphi}(s(u))$ as

•

$\tilde{\rho}^{\pi}((s,t))=\rho^{\pi}((s,t))$
•

$\tilde{\rho}^{\neg\pi}((s,t))=\rho^{\neg\pi}((s,t))$
•

$\tilde{\rho}^{\varphi_{1}\land\varphi_{2}}((s,t))\leq\rho^{\varphi_{1}\land\varphi_{2}}((s,t))$
•

$\tilde{\rho}^{\varphi_{1}\lor\varphi_{2}}((s,t))\leq\rho^{\varphi_{1}\lor\varphi_{2}}((s,t))$
•

$\tilde{\rho}^{\mathbf{F}_{[t_{1},t_{2}]}\varphi}((s,t))\leq\rho^{\mathbf{F}_{[t_{1},t_{2}]}\varphi}((s,t))$
•

$\tilde{\rho}^{\mathbf{G}_{[t_{1},t_{2}]}\varphi}((s,t))\leq\rho^{\mathbf{G}_{[t_{1},t_{2}]}\varphi}((s,t))$
•

$\tilde{\rho}^{\varphi_{1}\mathbf{U}_{[t_{1},t_{2}]}\varphi_{2}}((s,t))\leq\rho^{\varphi_{1}\mathbf{U}_{[t_{1},t_{2}]}\varphi_{2}}((s,t))$ .

Moreover, according to Lm. 2, the approximation errors associated with the operators in (15) are bounded and also vanishes as $k_{1},k_{2}\rightarrow\infty$ . Therefore, the approximation error associated with the SRM2 should follow (21). ∎

The above lemma implies that the actual (non-smooth) robustness measure $\rho^{\varphi}(s(u))$ with respect to the SRM2 $\tilde{\rho}^{\varphi}(s(u))$ is placed such that

\tilde{\rho}^{\varphi}(s(u))\leq\rho^{\varphi}(s(u))\leq\tilde{\rho}^{\varphi}(s(u))+U_{k}^{\varphi}.

Therefore, in this scenario (SRM2), achieving $\tilde{\rho}^{\varphi}(s(u))>0$ guarantees the satisfaction of the specification, i.e.,

\tilde{\rho}^{\varphi}(s(u))>0\implies\rho^{\varphi}(s(u))>0\implies s(u)\vDash\varphi.

This indeed is the soundness property promised earlier. Hence, it is clear that the SRM2 proposed in [20] is sound and also asymptotically reverse-sound and asymptotically complete.

Even though having a sound SRM (e.g., SRM2) is important in verification type problems, in falsification type problems (where the aim is to find a control that violates a given specification), it is critical to have a reverse-sound SRM. Further, since a reverse-sound SRM will, by definition, over-approximate the actual robustness measure (as opposed to a sound SRM that under-approximates the actual robustness measure), one can expect to use a sound SRM together with a reverse-sound SRM (e.g., use one as a “boosting” objective function for the other [23]) to achieve better and more decisive results. Motivated by these prospects, in the same spirit of the SRM2, here we propose a new SRM (labeled as SRM3) that recovers the lacking reverse-soundness property in SRM1 [21], while also preserving the asymptotic soundness and asymptotic completeness properties in SRM1 [21].

The proposed SRM3 is defined using $k_{1}$ -Soft- $\min$ and $k_{2}$ -Quasi- $\max$ operators (see Tab. I):

	$\displaystyle\widetilde{\min}\{a\}=$	$\displaystyle\frac{\sum_{i=1}^{m}a_{i}e^{-k_{1}a_{i}}}{\sum_{i=1}^{m}e^{-k_{1}a_{i}}}\mbox{ and}$		(22)
	$\displaystyle\widetilde{\max}\{a\}=$	$\displaystyle\frac{1}{k_{2}}\log\left(\sum_{i=1}^{m}e^{k_{2}a_{i}}\right),$		(22)

as smooth-min and smooth-max operators, respectively. Similar to before, the above operators are smooth everywhere, and their respective gradients can be found in Tab. I. The following lemma establishes the bounds on the approximation error associates with the operators in (22).

The smooth-min and smooth-max operators in (22) satisfy the following respective approximation error bounds:

$\displaystyle(\min\{a\}-\widetilde{\min}\{a\})\in$	$\displaystyle[-(a_{1}-a_{m})(1-\frac{1}{\sum_{i=1}^{m}e^{-k_{1}(a_{i}-a_{m})}}),\,0]$	(23)
$\displaystyle\subseteq$	$\displaystyle[-\frac{a_{1}-a_{m}}{1+\frac{e^{k_{1}(a_{m-1}-a_{m})}}{m-1}},\,0]\mbox{ and }$
$\displaystyle(\max\{a\}-\widetilde{\max}\{a\})\in$	$\displaystyle[-\frac{1}{k_{2}}\log(1+(m-1)e^{-k_{2}(a_{1}-a_{2})}),\,0]$
$\displaystyle\subseteq$	$\displaystyle[-\frac{\log(m)}{k_{2}},\,0]$

The first result in (23) can be proved by following the same steps used in the proof of the second statement in (16) in Lm. 2. The second result in (23) has already been proven in Lm. 1. ∎

In parallel to Lm. 3, the following lemma can be established regarding the approximation error associated with the SRM3 $\tilde{\rho}^{\varphi}(s(u))$ defined by the operators in (22).

The approximation error associated with the SRM3 $\tilde{\rho}^{\varphi}(s(u))$ is bounded such that

(\rho^{\varphi}(s(u))-\tilde{\rho}^{\varphi}(s(u)))\in[L_{k}^{\varphi},0],

(24)

where $L_{k}^{\varphi}$ is some negative real number dependent on the specification $\varphi$ and the parameters $k=[k_{1},k_{2}]$ , and $L_{k}^{\varphi}\rightarrow 0$ as $k_{1},k_{2}\rightarrow\infty$ .

The proof follows the same steps as that of Lm. 3, and is, therefore, omitted. ∎

The above lemma implies that the actual (non-smooth) robustness measure $\rho^{\varphi}(s(u))$ lies in the range:

\tilde{\rho}^{\varphi}(s(u))+L_{k}^{\varphi}\leq\rho^{\varphi}(s(u))\leq\tilde{\rho}^{\varphi}(s(u)),

Hence, in this scenario (SRM3), achieving $\tilde{\rho}^{\varphi}(s(u))<0$ implies a violation of the specification (i.e., $s(u)\nvDash\varphi$ ). i.e.,

\tilde{\rho}^{\varphi}(s(u))<0\implies\rho^{\varphi}(s(u))<0\implies s(u)\nvDash\varphi.

This indeed is the reverse-soundness property promised earlier. Therefore, it is clear that the proposed SRM3 is reverse sound and also asymptotically sound and asymptotically complete.

As a complementary approach for the SRM1 [21], we now propose a new SRM (labeled SRM4). In particular, this SRM4 is defined using the $k_{1}$ -Soft- $\min$ and $k_{2}$ -Soft- $\max$ operators (see Tab I):

	$\displaystyle\widetilde{\min}\{a\}=$	$\displaystyle\frac{\sum_{i=1}^{m}a_{i}e^{-k_{1}a_{i}}}{\sum_{i=1}^{m}e^{-k_{1}a_{i}}}\mbox{ and}$		(25)
	$\displaystyle\widetilde{\max}\{a\}=$	$\displaystyle\frac{\sum_{i=1}^{m}a_{i}e^{k_{2}a_{i}}}{\sum_{i=1}^{m}e^{k_{2}a_{i}}},$		(25)

as smooth-min and smooth-max operators, respectively.

Compared to the smooth-min and smooth-max operators used in SRM1 (given in (8)), the operators in (25) have a special property: when $k_{1},k_{2}\rightarrow 0$ , both operators converge to the arithmetic mean operator. According to the findings in [7], optimizing a robustness measure computed based on mean-like (e.g., arithmetic mean) operators rather than min/max-like (e.g., smooth-min/max) operators can lead to more uniformly robust solutions. This is because, while the latter (min/max-based) approach optimizes the minimum margin of satisfaction of all the specification components (e.g., predicates), the former (mean-based) approach optimizes the mean margin of satisfaction of all the specification components. Hence, one can expect to use the SRM1 (with moderate $k_{1},k_{2}$ values) together with the SRM4 (with low $k_{1},k_{2}$ values) to reach more uniformly robust solutions (e.g., use SRM4 as a “boosting” objective function for the SRM1 [23]). Even when used alone, intuitively, the SRM4 (with moderate $k_{1},k_{2}$ values) can be expected to provide more uniformly robust solutions.

Similar to previous SRMs, the above operators are smooth everywhere, and their respective gradients are provided in Tab I. The following lemma establishes the bounds on the approximation errors associated with the operators in (25).

The smooth-min and smooth-max operators in (25) satisfy the following respective approximation error bounds:

$\displaystyle(\min\{a\}-\widetilde{\min}\{a\})\in$	$\displaystyle[-(a_{1}-a_{m})(1-\frac{1}{\sum_{i=1}^{m}e^{-k_{1}(a_{i}-a_{m})}}),\,0]$	(26)
$\displaystyle\subseteq$	$\displaystyle[-\frac{a_{1}-a_{m}}{1+\frac{e^{k_{1}(a_{m-1}-a_{m})}}{m-1}},\,0]\mbox{ and }$
$\displaystyle(\max\{a\}-\widetilde{\max}\{a\})\in$	$\displaystyle[0,\,(a_{1}-a_{m})(1-\frac{1}{\sum_{i=1}^{m}e^{-k_{2}(a_{1}-a_{i})}})]$
$\displaystyle\subseteq$	$\displaystyle[0,\,\frac{a_{1}-a_{m}}{1+\frac{e^{k_{2}(a_{1}-a_{2})}}{m-1}}].$

The both results in (26) has already been proven in Lms. 2 and 4. ∎

From the above lemma, it is clear that the approximation errors associated with the smooth-min and smooth-max operators in (25) are bounded and also vanishes as $k_{1},k_{2}\rightarrow\infty$ . Therefore, similar to the case with the SRM1, the approximation error associated with the SRM4 can be bounded as

(\rho^{\varphi}(s(u))-\tilde{\rho}^{\varphi}(s(u))\in[L_{k}^{\varphi},U_{k}^{\varphi}],

(27)

i.e., the actual robustness measure $\rho^{\varphi}(s(u))$ is such that

\tilde{\rho}^{\varphi}(s(u))+L_{k}^{\varphi}\leq\rho^{\varphi}(y,x,u)\leq\tilde{\rho}^{\varphi}(s(u))+U_{k}^{\varphi},

(28)

where $L_{k}^{\varphi}$ and $U_{k}^{\varphi}$ are two real numbers dependent on the STL specification $\varphi$ and the parameters $k=[k_{1},k_{2}]$ . The exact details on how $L_{k}^{\varphi}$ and $U_{k}^{\varphi}$ can be computed are provided in Section IV. Regardless, it should be clear that $k_{1},k_{2}\rightarrow\infty\implies L_{k}^{\varphi},U_{k}^{\varphi}\rightarrow 0$ . Therefore, similar to the SRM1, the SRM4 is asymptotically sound, asymptotically reverse-sound and asymptotically complete.

In the previous section, we discussed four candidate smooth robustness measures $\tilde{\rho}^{\varphi}(s)$ (SRM1-4) that can be used to approximate the actual non-smooth robustness measure $\rho^{\varphi}(s)$ when solving the synthesis problem (6) via a gradient-based optimization method. For notational convenience, let us define the corresponding approximation error as

\tilde{e}^{\varphi}(s)\triangleq(\rho^{\varphi}(s)-\tilde{\rho}^{\varphi}(s)).

(29)

As shown in (13), (21), (24) and (27) (obtained via Lms. 1, 2, 4 and 6, respectively), this approximation error $\tilde{e}^{\varphi}(s)$ will always be bounded inside some finite interval (henceforth called an error bound) of the form:

\tilde{e}^{\varphi}(s)\in[L_{\theta}^{\varphi},U_{\theta}^{\varphi}]\subset\mathbb{R},

(30)

irrespective of the signal $s=s(u)$ . Here, $L_{\theta}^{\varphi}$ and $U_{\theta}^{\varphi}$ are two real numbers where $\theta$ can be thought of as a collection of all the used smooth-min and smooth-max operator parameters (e.g., $\theta=[k_{1},k_{2}]$ ). Intuitively, this error bound $[L_{\theta}^{\varphi},U_{\theta}^{\varphi}]$ will depend on: 1) the specification $\varphi$ , 2) the SRM (i.e., the used smooth-min and smooth-max operator configuration: (8), (15), (22) or (25)), and 3) the smooth-min and smooth-max operator parameters $\theta$ .

In this section, we develop a set of semantics (parallel to the ones in Def. 2) to explicitly derive the error bound $[L_{\theta}^{\varphi},U_{\theta}^{\varphi}]$ in (30) for a given specification and an SRM - in terms of the operator parameters $\theta$ . Having this knowledge is critical as it enables one to sensibly select: 1) the SRM to optimize (in (6)), and 2) the operator parameters $\theta$ . For example, one can select an SRM and its operator parameters $\theta$ that minimizes the width of the error bound, i.e., $U_{\theta}^{\varphi}-L_{\theta}^{\varphi}$ .

In the following analysis, we use the notation

	$\displaystyle(\min\{a\}-\widetilde{\min}\{a\})\in$	$\displaystyle[L_{k_{1},m}^{\min},\ U_{k_{1},m}^{\min}]\mbox{ and }$		(31)
	$\displaystyle(\max\{a\}-\widetilde{\max}\{a\})\in$	$\displaystyle[L_{k_{2},m}^{\max},\ U_{k_{2},m}^{\max}],$		(31)

to commonly represent the approximation error bounds associated with different possible respective smooth-min and smooth-max operators proven in Lms. 1, 2, 4, 6 (also outlined in Tab. I). Note also that, in (31), $m$ is the cardinality of the set $\bar{a}$ and $k_{1},k_{2}\in\mathbb{R}_{>0}$ are operator parameters that a user needs to select. For example, if the SRM1 is to be used,

	$\displaystyle[L_{k_{1},m}^{\min},\ U_{k_{1},m}^{\min}]\equiv$	$\displaystyle[0,\ \frac{\log(m)}{k_{1}}],\mbox{ and }$
	$\displaystyle[L_{k_{2},m}^{\max},\ U_{k_{2},m}^{\max}]\equiv$	$\displaystyle[-\frac{\log(m)}{k_{2}},\ 0].$

We also require the following minor theoretical result.

If $a_{i},\tilde{a}_{i},L_{i},U_{i}\in\mathbb{R}$ are such that $(a_{i}-\tilde{a}_{i})\in[L_{i},U_{i}]$ for all $i\in[1,m]\ (\triangleq\{1,2,\ldots,m\})$ , then

	$\displaystyle\left(\underset{i\in[1,m]}{\min}\{a_{i}\}-\underset{i\in[1,m]}{\min}\{\tilde{a}_{i}\}\right)\in\left[\underset{i\in[1,m]}{\min}\{L_{i}\},\ \ \underset{i\in[1,m]}{\max}\{U_{i}\}\right],$		(32)
	$\displaystyle\left(\underset{i\in[1,m]}{\max}\{a_{i}\}-\underset{i\in[1,m]}{\max}\{\tilde{a}_{i}\}\right)\in\left[\underset{i\in[1,m]}{\min}\{L_{i}\},\ \ \underset{i\in[1,m]}{\max}\{U_{i}\}\right].$		(32)

To prove the first result, take $a_{j}=\min_{i\in[1,m]}\{a_{i}\}$ and $\tilde{a}_{k}=\min_{i\in[1,m]}\{\tilde{a}_{i}\}$ where $j,k\in[1,m]$ . According to this definition, $a_{j}\leq a_{k}$ and $\tilde{a}_{k}\leq\tilde{a}_{j}$ . Also, according to the given information, $(a_{j}-\tilde{a}_{j})\geq L_{j}$ and $(a_{k}-\tilde{a}_{k})\leq U_{k}$ . We now can use these relationships to impose bounds on $(a_{j}-\tilde{a}_{k})$ as:

	$\displaystyle(a_{j}-\tilde{a}_{k})$	$\displaystyle\geq(a_{j}-\tilde{a}_{j})\geq L_{j}\geq\min_{i\in[1,m]}\{L_{i}\},\mbox{ and }$
	$\displaystyle(a_{j}-\tilde{a}_{k})$	$\displaystyle\leq(a_{k}-\tilde{a}_{k})\leq U_{k}\leq\max_{i\in[1,m]}\{U_{i}\}.$

This proves the first result in (32). Following the same steps, the second result in (32) can be established. ∎

Finally, we improve the generality of the proposing set of semantics (that computes the error bound $[L_{\theta}^{\varphi},U_{\theta}^{\varphi}]$ in (30)) by introducing a small modification to the smooth STL robust semantics given in Def. 2. In particular, we replace the first smooth STL robust semantic: $\tilde{\rho}^{\pi}(s)=\mu^{\pi}(s_{t})$ by a noise affected version of it:

\tilde{\rho}^{\pi}((s,t))=\mu^{\pi}(s_{t})+w^{\pi}(s_{t}),

(33)

where the noise term $w^{\pi}(s_{t})$ is such that $w^{\pi}(s_{t})\in[L^{\pi}(s_{t}),U^{\pi}(s_{t})]$ with known functions $L^{\pi}:\mathbb{R}^{p}\rightarrow\mathbb{R}$ and $U^{\pi}:\mathbb{R}^{p}\rightarrow\mathbb{R}$ . For example, $L^{\pi}(s_{t})=-U^{\pi}(s_{t})=-\epsilon$ where $\epsilon\in\mathbb{R}_{>0}$ is a known constant, is a possibility. Intuitively, this modification causes the error bound $[L_{\theta}^{\varphi},U_{\theta}^{\varphi}]$ in (30) to become dependent on the signal $s$ , i.e., now,

\tilde{e}^{\varphi}(s)\triangleq(\rho^{\varphi}(s)-\tilde{\rho}^{\varphi}(s))\in[L_{\theta}^{\varphi}(s),U_{\theta}^{\varphi}(s)].

(34)

Therefore, this modification complicates the task at hand: computing the error bound $[L_{\theta}^{\varphi}(s),U_{\theta}^{\varphi}(s)]$ . However, as we will see in the sequel, it allows us to see how the uncertainties in the mission space can affect this error bound $[L_{\theta}^{\varphi}(s),U_{\theta}^{\varphi}(s)]$ .

If there are no uncertainties in the mission space, one can simply set $L^{\pi}(s_{t})=U^{\pi}(s_{t})=0$ in (33) for all $s_{t}$ and for all predicates $\pi$ . Moreover, if such uncertainties are independent of the agent trajectory $s$ , one can simply set $L^{\pi}(s_{t})=L^{\pi}$ and $U^{\pi}(s_{t})=U^{\pi}$ where $L^{\pi}$ and $U^{\pi}$ are known constants. In both of these occasions, the resulting error bound $[L_{\theta}^{\varphi}(s),U_{\theta}^{\varphi}(s)]$ will be independent of the signal $s$ . Evaluating such a signal independent error bound is a reasonable thing to do, especially in an off-line stage where the signal $s$ is unknown and the focus is on sensibly selecting an SRM along with its operator parameters $\theta$ .

Consider the set of semantics (we named the STL error semantics) defined in the following definition.

(STL Error Semantics)

•

$\tilde{e}^{\pi}((s,t))\in[-U^{\pi}(s_{t}),\ -L^{\pi}(s_{t})]$
•

$\tilde{e}^{\neg\pi}((s,t))\in[L^{\pi}(s_{t}),\ U^{\pi}(s_{t})]$
•

$\tilde{e}^{\varphi_{1}\land\varphi_{2}}((s,t))\in[L_{k_{1},2}^{\min}+\min\{L_{\theta_{1}}^{\varphi_{1}}((s,t)),L_{\theta_{2}}^{\varphi_{2}}((s,t))\},\$
$U_{k_{1},2}^{\min}+\max\{U_{\theta_{1}}^{\varphi_{1}}((s,t)),U_{\theta_{2}}^{\varphi_{2}}((s,t))\}]$
•

$\tilde{e}^{\varphi_{1}\lor\varphi_{2}}((s,t))\in[L_{k_{2},2}^{\max}+\min\{L_{\theta_{1}}^{\varphi_{1}}((s,t)),L_{\theta_{2}}^{\varphi_{2}}((s,t))\},\$
$U_{k_{2},2}^{\max}+\max\{U_{\theta_{1}}^{\varphi_{1}}((s,t)),U_{\theta_{2}}^{\varphi_{2}}((s,t))\}]$
•

$\tilde{e}^{\mathbf{F}_{[t_{1},t_{2}]}\varphi}((s,t))\in[L_{k_{2},t_{2}-t_{1}+1}^{\max}+\min_{\tau\in[t+t_{1},t+t_{2}]}\{$
$L_{\theta}^{\varphi}((s,\tau))\},\ U_{k_{2},t_{2}-t_{1}+1}^{\max}+\max_{\tau\in[t+t_{1},t+t_{2}]}\{U_{\theta}^{\varphi}((s,\tau))\}]$
•

$\tilde{e}^{\mathbf{G}_{[t_{1},t_{2}]}\varphi}((s,t))\in[L_{k_{1},t_{2}-t_{1}+1}^{\min}+\min_{\tau\in[t+t_{1},t+t_{2}]}\{$
$L_{\theta}^{\varphi}((s,\tau))\},\ U_{k_{1},t_{2}-t_{1}+1}^{\min}+\max_{\tau\in[t+t_{1},t+t_{2}]}\{U_{\theta}^{\varphi}((s,\tau))\}]$
•

$\tilde{e}^{\varphi_{1}\mathbf{U}_{[t_{1},t_{2}]}\varphi_{2}}((s,t))\in[L_{k_{2},t_{2}-t_{1}+1}^{\max}+\min_{\tau\in[t+t_{1},t+t_{2}]}\{$
$L_{\theta_{4}}^{\varphi_{4}}((s,\tau))\},U_{k_{2},t_{2}-t_{1}+1}^{\max}+\max_{\tau\in[t+t_{1},t+t_{2}]}\{U_{\theta_{4}}^{\varphi_{4}}((s,\tau))\}]$
where
$[L_{\theta_{4}}^{\varphi_{4}}((s,\tau)),U_{\theta_{4}}^{\varphi_{4}}((s,\tau))]\equiv\ [L_{k_{1},2}^{\min}+\min\{L_{\theta_{1}}^{\varphi_{1}}((s,\tau)),$
$L_{\theta_{3}}^{\varphi_{3}}((s,\tau))\},U_{k_{1},2}^{\min}+\max\{U_{\theta_{1}}^{\varphi_{1}}((s,\tau)),U_{\theta_{3}}^{\varphi_{3}}((s,\tau))\}],$
$[L_{\theta_{3}}^{\varphi_{3}}((s,\tau)),U_{\theta_{3}}^{\varphi_{3}}((s,\tau))]\equiv\ [L_{k_{1},\tau-t-t_{1}+1}+\min_{\delta\in[t+t_{1},\tau]}$
$\{L_{\theta_{2}}^{\varphi_{2}}((s,\delta))\},U_{k_{1},\tau-t-t_{1}+1}+\max_{\delta\in[t+t_{1},\tau]}\{U_{\theta_{2}}^{\varphi_{2}}((s,\delta))\}]$ .

For a known signal suffix $(s,t)$ , a specification $\varphi$ and a smooth robustness measure (SRM1-4), the STL error semantics in Def. 2 can be used to determine the approximation error bound

[L_{\theta}^{\varphi}((s,t)),U_{\theta}^{\varphi}((s,t))]\ni\tilde{e}^{\varphi}((s,t))\triangleq(\rho^{\varphi}((s,t))-\tilde{\rho}^{\varphi}((s,t))),

(the same as (34)) in terms of the used collection of smooth-min and smooth-max operator parameters $\theta$ .

Here, we need to prove each semantic in Def. 4 using the respective semantics in Defs. 1 and 2.

According to Defs. 1 and 2, $\rho^{\pi}((s,t))=\mu^{\pi}(s_{t})$ and $\tilde{\rho}^{\pi}((s,t))=\mu^{\pi}(s_{t})+w^{\pi}(s_{t})$ (recall (33)), respectively. Therefore, the corresponding approximation error is $\tilde{e}^{\pi}((s,t))\triangleq(\rho^{\pi}((s,t))-\tilde{\rho}^{\pi}((s,t)))=-w^{\pi}(s_{t}).$ Since $w^{\pi}(s_{t})\in[L^{\pi}(s_{t}),U^{\pi}(s_{t})]$ (from (33)), it is easy to see that $\tilde{e}^{\pi}((s,t))\in[-U^{\pi}(s_{t}),-L^{\pi}(s_{t})]$ (i.e., the Semantic 1).

Can be proved using the same steps as above.

According to the corresponding semantics in Defs. 1 and 2, $\rho^{\varphi_{1}\land\varphi_{2}}((s,t))=\min\{\rho^{\varphi_{1}}((s,t)),\rho^{\varphi_{2}}((s,t))\}$ and $\tilde{\rho}^{\varphi_{1}\land\varphi_{2}}((s,t))=\widetilde{\min}\{\tilde{\rho}^{\varphi_{1}}((s,t)),\tilde{\rho}^{\varphi_{2}}((s,t))\}$ , respectively. Therefore, the corresponding approximation error is $\tilde{e}^{\varphi_{1}\land\varphi_{2}}((s,t))\triangleq(\rho^{\varphi_{1}\land\varphi_{2}}((s,t))-\tilde{\rho}^{\varphi_{1}\land\varphi_{2}}((s,t)))=\min\{\rho^{\varphi_{1}}((s,t)),\,\rho^{\varphi_{2}}((s,t))\}-\widetilde{\min}\{\tilde{\rho}^{\varphi_{1}}((s,t)),\,\tilde{\rho}^{\varphi_{2}}((s,t))\}$ .

To bound this error term $\tilde{e}^{\varphi_{1}\land\varphi_{2}}((s,t))$ , what we have at our disposal are the error bounds: $[L_{\theta_{i}}^{\varphi_{i}}((s,t)),U_{\theta_{i}}^{\varphi_{i}}((s,t))]\ni\tilde{e}^{\varphi_{i}}((s,t))\triangleq(\rho^{\varphi_{i}}((s,t))-\tilde{\rho}^{\varphi_{i}}((s,t)))$ , for $i=1,2.$ Applying these two error bounds in Lm 7, we get

	$\displaystyle\min\{\rho^{\varphi_{1}}((s,t)),\,\rho^{\varphi_{2}}((s,t))\}-\min\{\tilde{\rho}^{\varphi_{1}}((s,t)),\,\tilde{\rho}^{\varphi_{2}}((s,t))\}$		(35)
	$\displaystyle\in[\min\{L_{\theta_{1}}^{\varphi_{1}}((s,t)),L_{\theta_{2}}^{\varphi_{2}}((s,t))\},$
	$\displaystyle\max\{U_{\theta_{1}}^{\varphi_{1}}((s,t)),U_{\theta_{2}}^{\varphi_{2}}((s,t))\}].$

Further, using (31), we can write

	$\displaystyle\min\{\tilde{\rho}^{\varphi_{1}}((s,t)),\tilde{\rho}^{\varphi_{2}}((s,t))\}-\widetilde{\min}\{\tilde{\rho}^{\varphi_{1}}((s,t)),\,\tilde{\rho}^{\varphi_{2}}((s,t))\}$		(36)
	$\displaystyle\in[L_{k_{1},2}^{\min},U_{k_{1},2}^{\min}].$		(36)

Finally, by adding (35) and (36) we can obtain a bound for the approximation error term $\tilde{e}^{\varphi_{1}\land\varphi_{2}}((s,t))$ as

	$\displaystyle\tilde{e}^{\varphi_{1}\land\varphi_{2}}((s,t))\in$	$\displaystyle\ [L_{\theta}^{\varphi_{1}\land\varphi_{2}}((s,t)),\ U_{\theta}^{\varphi_{1}\land\varphi_{2}}((s,t))]$
	$\displaystyle\equiv$	$\displaystyle\ [L_{k_{1},2}^{\min}+\min\{L_{\theta_{1}}^{\varphi_{1}}((s,t)),L_{\theta_{2}}^{\varphi_{2}}((s,t))\},$
		$\displaystyle\ \ U_{k_{1},2}^{\min}+\max\{U_{\theta_{1}}^{\varphi_{1}}((s,t)),U_{\theta_{2}}^{\varphi_{2}}((s,t))\}],$

where $\theta=\theta_{1}\cup\theta_{2}\cup\{k_{1}\}$ (which makes it clear how the collection of operator parameters $\theta$ grows with the depth of the specification). This proves the Semantic 3.

Can be proved using the same steps as above.

Similar to before, by subtracting the corresponding semantics in Defs. 1, 2, we get the error term

	$\displaystyle\tilde{e}^{\mathbf{F}_{[t_{1},t_{2}]}\varphi}((s,t))\triangleq\rho^{\mathbf{F}_{[t_{1},t_{2}]}\varphi}((s,t))-\tilde{\rho}^{\mathbf{F}_{[t_{1},t_{2}]}\varphi}((s,t))$		(37)
	$\displaystyle=\max_{\tau\in[t+t_{1},t+t_{2}]}\{\rho^{\varphi}((s,\tau))\}-\underset{\tau\in[t+t_{1},t+t_{2}]}{\widetilde{\max}}\{\tilde{\rho}^{\varphi}((s,\tau))\}.$		(37)

To bound this error term $\tilde{e}^{\mathbf{F}_{[t_{1},t_{2}]}\varphi}((s,t))$ , what we have at our disposal are the bounds: $[L_{\theta}^{\varphi}((s,\tau)),U_{\theta}^{\varphi}((s,\tau))]\ni\tilde{e}^{\varphi}((s,\tau))\triangleq(\rho^{\varphi}((s,\tau))-\tilde{\rho}^{\varphi}((s,\tau)))$ , for all $\tau\in[t+t_{1},t+t_{2}]$ . Applying these error bounds in Lm 7, we get

	$\displaystyle\max_{\tau\in[t+t_{1},t+t_{2}]}\{\rho^{\varphi}((s,\tau))\}-\max_{\tau\in[t+t_{1},t+t_{2}]}\{\tilde{\rho}^{\varphi}((s,\tau))\}$		(38)
	$\displaystyle\in[\min_{\tau\in[t+t_{1},t+t_{2}]}\{L_{\theta}^{\varphi}((s,\tau))\},\ \max_{\tau\in[t+t_{1},t+t_{2}]}\{U_{\theta}^{\varphi}((s,\tau))\}].$		(38)

Further, using (31), we can write

	$\displaystyle\max_{\tau\in[t+t_{1},t+t_{2}]}\{\tilde{\rho}^{\varphi}((s,\tau))\}-\underset{\tau\in[t+t_{1},t+t_{2}]}{\widetilde{\max}}\{\tilde{\rho}^{\varphi}((s,\tau))\}$		(39)
	$\displaystyle\in[L_{k_{2},t_{2}-t_{1}+1}^{\max},U_{k_{2},t_{2}-t_{1}+1}^{\max}]$		(39)

Finally, by adding (38) and (39) we can obtain a bound for the approximation error term $\tilde{e}^{\mathbf{F}_{[t_{1},t_{2}]}\varphi}((s,t))$ as

$\displaystyle\tilde{e}^{\mathbf{F}_{[t_{1},t_{2}]}\varphi}((s,t))$	$\displaystyle\equiv[L_{\theta^{\prime}}^{\mathbf{F}_{[t_{1},t_{2}]}\varphi}((s,t)),\ U_{\theta^{\prime}}^{\mathbf{F}_{[t_{1},t_{2}]}\varphi}((s,t))],$	(40)
	$\displaystyle\in[L_{k_{2},t_{2}-t_{1}+1}^{\max}+\min_{\tau\in[t+t_{1},t+t_{2}]}\{L_{\theta}^{\varphi}((s,\tau))\},$
	$\displaystyle\ \ \ \ \ U_{k_{2},t_{2}-t_{1}+1}^{\max}+\max_{\tau\in[t+t_{1},t+t_{2}]}\{U_{\theta}^{\varphi}((s,\tau))\}]$

where $\theta^{\prime}=\theta\cup\{k_{2}\}$ . This proves the Semantic 5.

Can be proved by combining the techniques used to prove Semantics 3, 5 and 6. Due to space constraints, details are omitted here. This completes the proof of Th. 1. ∎

Note that we are not constrained to use the same $k_{1},k_{2}$ parameter values across all the smooth-min, smooth-max operators required when defining an SRM for a specification. In other words, at different levels of the specification, different $k_{1},k_{2}$ values can be used. Having this flexibility is especially useful when the components of the specification are not properly normalized. One such example, identified using the proposed STL error semantics, is discussed in Section VI.

To conclude this section, we propose the following set of semantics (we named the Supplementary STL error semantics) applicable for a situation: 1) where there are no mission space uncertainties (i.e., when $L^{\pi}(s_{t})=U^{\pi}(s_{t})=0,\forall s_{t},\forall\pi$ in (33)), or, 2) where mission space uncertainties are independent of the agent trajectory $s$ (i.e., when $L^{\pi}(s_{t})=L^{\pi}$ and $U^{\pi}(s_{t})=U^{\pi}$ where $L^{\pi}$ and $U^{\pi}$ are known constants). As pointed out in Remark 2, in such scenarios, the resulting error bounds will be independent of the signal $s$ . This property is more evident in the semantics defined below (compared to the semantics defined in Def. 4).

(Supplementary STL Error Semantics)

•

$\tilde{e}^{\pi}\in[-U^{\pi},\ -L^{\pi}]$
•

$\tilde{e}^{\neg\pi}\in[L^{\pi},\ U^{\pi}]$
•

$\tilde{e}^{\varphi_{1}\land\varphi_{2}}\in[L_{k_{1},2}^{\min}+\min\{L_{\theta_{1}}^{\varphi_{1}},L_{\theta_{2}}^{\varphi_{2}}\},\ U_{k_{1},2}^{\min}$
$+\max\{U_{\theta_{1}}^{\varphi_{1}},U_{\theta_{2}}^{\varphi_{2}}\}]$
•

$\tilde{e}^{\varphi_{1}\lor\varphi_{2}}\in[L_{k_{2},2}^{\max}+\min\{L_{\theta_{1}}^{\varphi_{1}},L_{\theta_{2}}^{\varphi_{2}}\},\ U_{k_{2},2}^{\max}$
$+\max\{U_{\theta_{1}}^{\varphi_{1}},U_{\theta_{2}}^{\varphi_{2}}\}]$
•

$\tilde{e}^{\mathbf{F}_{[t_{1},t_{2}]}\varphi}\in[L_{k_{2},t_{2}-t_{1}+1}^{\max}+L_{\theta}^{\varphi},\ U_{k_{2},t_{2}-t_{1}+1}^{\max}+U_{\theta}^{\varphi}]$
•

$\tilde{e}^{\mathbf{G}_{[t_{1},t_{2}]}\varphi}\in[L_{k_{1},t_{2}-t_{1}+1}^{\min}+L_{\theta}^{\varphi},\ U_{k_{1},t_{2}-t_{1}+1}^{\min}+U_{\theta}^{\varphi}]$
•

$\tilde{e}^{\varphi_{1}\mathbf{U}_{[t_{1},t_{2}]}\varphi_{2}}\in[L_{k_{2},t_{2}-t_{1}+1}^{\max}+L_{\theta_{4}}^{\varphi_{4}},\ U_{k_{2},t_{2}-t_{1}+1}^{\max}+U_{\theta_{4}}^{\varphi_{4}}]$
where
$[L_{\theta_{4}}^{\varphi_{4}},U_{\theta_{4}}^{\varphi_{4}}]\equiv\ [L_{k_{1},2}^{\min}+\min\{L_{\theta_{1}}^{\varphi_{1}},L_{\theta_{3}}^{\varphi_{3}}\},\ U_{k_{1},2}^{\min}$
$+\max\{U_{\theta_{1}}^{\varphi_{1}},U_{\theta_{3}}^{\varphi_{3}}\}],$
$[L_{\theta_{3}}^{\varphi_{3}},U_{\theta_{3}}^{\varphi_{3}}]\equiv\ [L_{k_{1},\tau-t-t_{1}+1}+L_{\theta_{2}}^{\varphi_{2}},\ U_{k_{1},\tau-t-t_{1}+1}+U_{\theta_{2}}^{\varphi_{2}}]$ .

For a given specification $\varphi$ and a smooth robustness measure (SRM1-4), the STL error semantics in Def. 5 can be used to determine the approximation error bound

[L_{\theta}^{\varphi},U_{\theta}^{\varphi}]\ni\tilde{e}^{\varphi}((s,t))\triangleq(\rho^{\varphi}((s,t))-\tilde{\rho}^{\varphi}((s,t))),

(the same as (30)) in terms of the used collection of smooth-min and smooth-max operator parameters $\theta$ .

The first two semantics in Def. 5 can be obtained by applying the relationships $L^{\pi}(s_{t})=L^{\pi}$ and $U^{\pi}(s_{t})=U^{\pi}$ in respective semantics in Def. 4. As a result of these first two semantics being independent of the signal suffix $(s,t)$ , all the remaining semantics in Def. 5 will also be independent of the signal suffice $(s,t)$ . These remaining semantics in Def. 5 can be proved by following the same steps used to establish their respective semantics in Def. 4. ∎

Recall that, in Section II, we formulated the interested synthesis problem (3) as an unconstrained optimization problem (6). Then, since the involved robustness measure objective $\rho^{\varphi}(s(u))$ in (6) is non-smooth, in Section III, we proposed to replace it with a smooth approximation (an SRM) $\tilde{\rho}^{\varphi}(s(u))$ inspired by the recent literature [21, 8, 7, 20]. The main motivation behind this replacement is to enable the use of efficient gradient-based optimization techniques to solve (6). Hence, the importance of knowing the gradient of the used SRM $\tilde{\rho}^{\varphi}(s(u))$ (with respect to $u$ ) is clear. However, to the best of the authors’ knowledge, experimental results reported in existing literature [21, 8, 7, 20] relies on numerically evaluated gradients rather than explicitly derived gradients (of SRMs). Intuitively, it is worth investigating the accuracy and the efficiency of such numerically evaluated gradients compared to explicitly derived gradients. Motivated by this need, in this section, we propose an efficient systematic approach to explicitly derive the gradient of the used SRM $\tilde{\rho}^{\varphi}(s(u))$ , i.e., $\frac{\partial\tilde{\rho}^{\varphi}(s(u))}{\partial u}$ .

First, notice that we can use the chain rule to write

\frac{\partial\tilde{\rho}^{\varphi}(s(u))}{\partial u}=\frac{\partial\tilde{\rho}^{\varphi}(s(u))}{\partial s}\frac{\partial s(u)}{\partial u}.

(41)

At this point, we remind that: 1) the SRM $\tilde{\rho}^{\varphi}(s(u))\in\mathbb{R}$ , 2) the composite signal $s(u)\triangleq\{s_{t}(u)\}_{t\in[0,T]}$ where $s_{t}(u)\triangleq[y_{t}^{\top}(u),x_{t}^{\top}(u),u_{t}^{\top}]^{\top}\in\mathbb{R}^{q}$ with $q\triangleq p+n+m$ , and 3) the control $u=\{u_{t}\}_{t\in[0,T]}$ where $u_{t}\in\mathbb{R}^{m}$ (all vectors are column vectors). For notational simplicity (also without any ambiguity), let us denote the three gradient terms in (41) as

\frac{\partial\tilde{\rho}^{\varphi}}{\partial u}\triangleq\frac{\partial\tilde{\rho}^{\varphi}(s(u))}{\partial u},\ \ \frac{\partial\tilde{\rho}^{\varphi}}{\partial s}\triangleq\frac{\partial\tilde{\rho}^{\varphi}(s(u))}{\partial s}\ \mbox{ and }\ \frac{\partial s}{\partial u}\triangleq\frac{\partial s(u)}{\partial u},

where $\tilde{\rho}^{\varphi}\in\mathbb{R}$ , $s\in\mathbb{R}^{(T+1)q}$ and $u\in\mathbb{R}^{(T+1)q}$ (consistent with the previously mentioned vector dimensions). Note that, the composition of these three gradient terms are as follows:

\frac{\partial\tilde{\rho}^{\varphi}}{\partial u}=\left[\frac{\partial\tilde{\rho}^{\varphi}}{\partial u_{0}},\frac{\partial\tilde{\rho}^{\varphi}}{\partial u_{1}},\ldots,\frac{\partial\tilde{\rho}^{\varphi}}{\partial u_{T}}\right]\in\mathbb{R}^{1\times(T+1)m},

(42)

where each $\frac{\partial\tilde{\rho}^{\varphi}}{\partial u_{t}}\in\mathbb{R}^{1\times m}$ for all $t\in[0,T]$ ,

\frac{\partial\tilde{\rho}^{\varphi}}{\partial s}=\left[\frac{\partial\tilde{\rho}^{\varphi}}{\partial s_{0}},\frac{\partial\tilde{\rho}^{\varphi}}{\partial s_{1}},\ldots,\frac{\partial\tilde{\rho}^{\varphi}}{\partial s_{T}}\right]\in\mathbb{R}^{1\times(T+1)q},

(43)

where each $\frac{\partial\tilde{\rho}^{\varphi}}{\partial s_{t}}\in\mathbb{R}^{1\times q}$ for all $t\in[0,T]$ and

\frac{\partial s}{\partial u}=\begin{bmatrix}\frac{\partial s_{0}}{\partial u_{0}}&\frac{\partial s_{0}}{\partial u_{1}}&\cdots&\frac{\partial s_{0}}{\partial u_{T}}\\ \frac{\partial s_{1}}{\partial u_{0}}&\frac{\partial s_{1}}{\partial u_{1}}&\cdots&\frac{\partial s_{1}}{\partial u_{T}}\\ \vdots&\vdots&\ddots&\vdots\\ \frac{\partial s_{T}}{\partial u_{0}}&\frac{\partial s_{T}}{\partial u_{1}}&\cdots&\frac{\partial s_{T}}{\partial u_{T}}\end{bmatrix}\in\mathbb{R}^{(T+1)q\times(T+1)m},

(44)

where each $\frac{\partial s_{t}}{\partial u_{\tau}}\in\mathbb{R}^{q\times m}$ for all $t,\tau\in[0,T]$ .

To obtain the interested gradient term $\frac{\partial\tilde{\rho}^{\varphi}}{\partial u}$ , we need to compute the gradient terms $\frac{\partial\tilde{\rho}^{\varphi}}{\partial s}$ and $\frac{\partial s}{\partial u}$ . For this purpose, in the following two subsections, we respectively propose a novel set of semantics and exploit the agent dynamics (1).

In the following analysis, we use the notation $0_{k}$ to represent the zero vector in $\mathbb{R}^{k}$ . Note also that, as shown in Tab. I, we already have derived the gradients of smooth-min and smooth-max operators (i.e., $\frac{\partial\widetilde{\min}\{a\}}{\partial a_{i}}$ , $\frac{\partial\widetilde{\max}\{a\}}{\partial a_{i}}\in\mathbb{R}$ , for all $i$ ) used in different SRMs: SRM1-4. Now, consider the set of semantics (we named the STL gradient semantics) defined below.

(STL gradient semantics)

•

$\frac{\partial\tilde{\rho}^{\pi}((s,t))}{\partial s}=\left[0_{tq}^{\top},\,\frac{\partial\mu^{\pi}(s_{t})}{\partial s_{t}},\,0_{(T-t)q}^{\top}\right]\in\mathbb{R}^{1\times(T+1)q}$
•

$\frac{\partial\tilde{\rho}^{\neg\pi}((s,t))}{\partial s}=-\frac{\partial\tilde{\rho}^{\pi}((s,t))}{\partial s}$
•

$\frac{\partial\tilde{\rho}^{\varphi_{1}\land\varphi_{2}}((s,t))}{\partial s}=\frac{\partial\widetilde{\min}\{\rho_{1},\rho_{2}\}}{\partial\rho_{1}}\frac{\partial\rho_{1}}{\partial s}+\frac{\partial\widetilde{\min}\{\rho_{1},\,\rho_{2}\}}{\partial\rho_{2}}\frac{\partial\rho_{2}}{\partial s}$
where $\rho_{1}\triangleq\tilde{\rho}^{\varphi_{1}}((s,t))$ and $\rho_{2}\triangleq\tilde{\rho}^{\varphi_{2}}((s,t))$
•

$\frac{\partial\tilde{\rho}^{\varphi_{1}\lor\varphi_{2}}((s,t))}{\partial s}=\frac{\partial\widetilde{\max}\{\rho_{1},\rho_{2}\}}{\partial\rho_{1}}\frac{\partial\rho_{1}}{\partial s}+\frac{\partial\widetilde{\max}\{\rho_{1},\,\rho_{2}\}}{\partial\rho_{2}}\frac{\partial\rho_{2}}{\partial s}$
where $\rho_{1}\triangleq\tilde{\rho}^{\varphi_{1}}((s,t))$ and $\rho_{2}\triangleq\tilde{\rho}^{\varphi_{2}}((s,t))$
•

$\frac{\partial\tilde{\rho}^{\mathbf{F}_{[t_{1},t_{2}]}\varphi}((s,t))}{\partial s}=\sum_{\tau\in[t+t_{1},t+t_{2}]}\frac{\partial\widetilde{\max}_{\tau\in[t+t_{1},t+t_{2}]}\{\rho_{\tau}\}}{\partial\rho_{\tau}}\frac{\partial\rho_{\tau}}{\partial s}$
where $\rho_{\tau}\triangleq\tilde{\rho}^{\varphi}((s,\tau))$ for any $\tau\in[t+t_{1},t+t_{2}]$
•

$\frac{\partial\tilde{\rho}^{\mathbf{G}_{[t_{1},t_{2}]}\varphi}((s,t))}{\partial s}=\sum_{\tau\in[t+t_{1},t+t_{2}]}\frac{\partial\widetilde{\min}_{\tau\in[t+t_{1},t+t_{2}]}\{\rho_{\tau}\}}{\partial\rho_{\tau}}\frac{\partial\rho_{\tau}}{\partial s}$
where $\rho_{\tau}\triangleq\tilde{\rho}^{\varphi}((s,\tau))$ for any $\tau\in[t+t_{1},t+t_{2}]$
•

$\frac{\partial\tilde{\rho}^{\varphi_{1}\mathbf{U}_{[t_{1},t_{2}]}\varphi_{2}}((s,t))}{\partial s}=\sum_{\tau\in[t+t_{1},t+t_{2}]}\frac{\partial\widetilde{\max}_{\tau\in[t+t_{1},t+t_{2}]}\{\rho_{\tau}\}}{\partial\rho_{\tau}}\frac{\partial\rho_{\tau}}{\partial s}$ ,
where $\frac{\partial\rho_{\tau}}{\partial s}=\frac{\partial\widetilde{\min}\{\rho_{1,\tau},\rho_{2,\tau}\}}{\rho_{1,\tau}}\frac{\partial\rho_{1,\tau}}{\partial s}+\frac{\partial\widetilde{\min}\{\rho_{1,\tau},\rho_{2,\tau}\}}{\rho_{2,\tau}}\frac{\partial\rho_{2,\tau}}{\partial s}$
and $\frac{\partial\rho_{2,\tau}}{\partial s}=\sum_{\delta\in[t+t_{1},\tau]}\frac{\partial\widetilde{\min}_{\delta\in[t+t_{1},\tau]}\{\rho_{2,\delta}\}}{\partial\rho_{2,\delta}}\frac{\partial\rho_{2,\delta}}{\partial s},$
with $\rho_{\tau}\triangleq\widetilde{\min}\{\rho_{1,\tau},\rho_{2,\tau}\}$ , $\rho_{1,\tau}\triangleq\tilde{\rho}^{\varphi_{1}}((s,\tau))$ ,
$\rho_{2,\tau}\triangleq\widetilde{\min}_{\delta\in[t+t_{1},\tau]}\{\rho_{2,\delta}\}$ and $\rho_{2,\delta}\triangleq\tilde{\rho}^{\varphi_{2}}((s,\delta))$ .

For a known signal suffix $(s,t)$ , a specification $\varphi$ and a smooth robustness measure (SRM1-4), the STL gradient semantics in Def. 6 can be used to determine the gradient $\frac{\partial\tilde{\rho}^{\varphi}((s,t))}{\partial s}$ (in the form: $\frac{\partial\tilde{\rho}^{\varphi}((s,t))}{\partial s}=[0_{tq}^{\top},\frac{\partial\tilde{\rho}^{\varphi}((s,t))}{\partial s_{t}},\ldots,\frac{\partial\tilde{\rho}^{\varphi}((s,t))}{\partial s_{T}}]\in\mathbb{R}^{1\times(T+1)q}$ ).

In Semantics 3-7 of Def. 6, note that all the involved gradient terms of smooth operator values are scalars (e.g., $\frac{\partial\widetilde{\min}\{\rho_{1},\rho_{2}\}}{\partial\rho_{1}},\,\frac{\partial\widetilde{\min}\{\rho_{1},\rho_{2}\}}{\partial\rho_{2}}\in\mathbb{R}$ in Semantic 3, see also Tab. I). Hence, in those semantics, such scalar gradients act only as scaling factors on the respective vector-valued constituent gradients (e.g., on $\frac{\partial\rho_{1}}{\partial s},\,\frac{\partial\rho_{2}}{\partial s}\in\mathbb{R}^{1\times(T+1)q}$ in Semantic 3). Therefore, the dimension of the resulting gradient upon using a Semantic 3-7 will be the same as that of the corresponding constituent gradients used. Now, since each such constituent gradient has its root in Semantic 1 - that always assigns a vector in $\mathbb{R}^{1\times(T+1)q}$ as the gradient value - it is clear that the semantics in Def. 6 will always produce a vector in $\mathbb{R}^{1\times(T+1)q}$ as the gradient $\frac{\partial\tilde{\rho}^{\varphi}((s,t))}{\partial s}$ .

In fact, each of the Semantics 3-7 in Def. 6 can be established easily by differentiating the respective semantic in Def. 2 (with respect to $s$ ) using the chain rule. For example, the Semantic 3 in Def. 6 is proved by differentiating the Semantic 3 in Def. 2 as

	$\displaystyle\frac{\partial\tilde{\rho}^{\varphi_{1}\land\varphi_{2}}((s,t))}{\partial s}=$	$\displaystyle\frac{\partial\widetilde{\min}\{\tilde{\rho}^{\varphi_{1}}((s,t)),\tilde{\rho}^{\varphi_{2}}((s,t))\}}{\partial s}$
	$\displaystyle=$	$\displaystyle\frac{\partial\widetilde{\min}\{\rho_{1},\rho_{2}\}}{\partial\rho_{1}}\frac{\partial\rho_{1}}{\partial s}+\frac{\partial\widetilde{\min}\{\rho_{1},\,\rho_{2}\}}{\partial\rho_{2}}\frac{\partial\rho_{2}}{\partial s}$

where $\rho_{1}\triangleq\tilde{\rho}^{\varphi_{1}}((s,t))$ and $\rho_{2}\triangleq\tilde{\rho}^{\varphi_{2}}((s,t))$ . Similarly, even without applying the chain rule, the Semantics 1-2 in Def. 6 can be proved by simply differentiating the respective semantics in Def. 2. Therefore, in parallel to the way that the semantics in Def. 2 computes the SRM $\tilde{\rho}^{\varphi}((s,t))$ , the semantics in Def. 6 computes the gradient of the SRM: $\frac{\partial\tilde{\rho}^{\varphi}((s,t))}{\partial s}$ . Finally, note that, by definition, $\tilde{\rho}^{\varphi}((s,t))=\tilde{\rho}^{\varphi}(\{s_{t},s_{t+1},\ldots,s_{T}\})$ and $s=(s,0)=\{s_{0},s_{1},\ldots,s_{T}\}$ . Hence, $\tilde{\rho}^{\varphi}((s,t))$ is independent of the signal values $\{s_{0},s_{1},\ldots,s_{t-1}\}$ , and thus, the first $tq$ terms in $\frac{\partial\tilde{\rho}^{\varphi}((s,t))}{\partial s}$ will always be zeros. This completes the proof. ∎

Finally, we point out that $\frac{\partial\tilde{\rho}^{\varphi}(s)}{\partial s}=\frac{\partial\tilde{\rho}^{\varphi}((s,0))}{\partial s}$ as $s=(s,0)$ . Hence, we now can use the STL gradient semantics proposed in Def. 6 (proved in Th. 1) to compute the gradient term $\frac{\partial\tilde{\rho}^{\varphi}(s)}{\partial s}$ required in (41). In the next section, we will derive the remaining gradient term required in (41), i.e., $\frac{\partial s(u)}{\partial u}$ .

In the following analysis, with regard to the agent dynamics model (1), we use the notation $\frac{\partial f}{\partial x}\big{|}_{t}$ to represent the $\frac{\partial f(x,u)}{\partial x}$ evaluated at $(x_{t},u_{t})$ where $t\in[0,T]$ . The same convention applies for the notations $\frac{\partial f}{\partial u}\big{|}_{t}$ , $\frac{\partial g}{\partial x}\big{|}_{t}$ and $\frac{\partial g}{\partial u}\big{|}_{t}$ . Since the functions $f(x,u)$ and $g(x,u)$ in (1) are assumed as a given and differentiable, their partial derivatives, i.e., $\frac{\partial f(x,u)}{\partial x}$ , $\frac{\partial f(x,u)}{\partial u}$ , $\frac{\partial g(x,u)}{\partial x}$ and $\frac{\partial g(x,u)}{\partial u}$ are also considered as a given. Therefore, for a given control signal $u=\{u_{t}\}_{t\in[0,T]}$ (which also determines the generated state signal $x=\{x_{t}\}_{t\in[0,T]}$ through (1)), terms like $\frac{\partial f}{\partial x}\big{|}_{t}$ , $\frac{\partial f}{\partial u}\big{|}_{t}$ , $\frac{\partial g}{\partial x}\big{|}_{t}$ and $\frac{\partial g}{\partial u}\big{|}_{t}$ can be evaluated efficiently for any $t\in[0,T]$ .

In order to determine the the required gradient term: $\frac{\partial s}{\partial u}=\frac{\partial s(u)}{\partial u}$ , we first need to establish the following two lemmas.

Under the agent dynamics model (1), the control input signal $u=\{u_{t}\}_{t\in[0,T]}$ and the output signal $y=\{y_{t}\}_{t\in[0,T]}$ are related such that, for all $t,\tau\in[0,T]$ ,

\frac{\partial y_{t}}{\partial u_{\tau}}=\begin{cases}\frac{\partial g}{\partial x}\big{|}_{t}\prod_{i=1}^{t-\tau-1}\left[\frac{\partial f}{\partial x}\Big{|}_{t-i}\right]\frac{\partial f}{\partial u}\Big{|}_{\tau},\ \ &\mbox{if }\tau<t,\\ \frac{\partial g}{\partial u}\big{|}_{t},\ \ &\mbox{if }\tau=t,\\ 0,\ \ &\mbox{if }\tau>t.\\ \end{cases}

(45)

According to the agent dynamics model (1),

$\displaystyle y_{t}=$	$\displaystyle g(x_{t},u_{t})$	(46)
$\displaystyle=$	$\displaystyle g(f(x_{t-1},u_{t-1}),u_{t})$
$\displaystyle=$	$\displaystyle g(f(f(x_{t-2},u_{t-2}),u_{t-1}),u_{t})$
$\displaystyle\vdots$

Therefore, $\frac{\partial y_{t}}{\partial u_{\tau}}=0$ for any $\tau>t$ and $\frac{\partial y_{t}}{\partial u_{t}}=\frac{\partial g}{\partial u}\big{|}_{t}$ . Similarly, using (46) together with the product rule, we can write

	$\displaystyle\frac{\partial y_{t}}{\partial u_{t-1}}=$	$\displaystyle\frac{\partial g}{\partial x}\Big{\|}_{t}\frac{\partial f}{\partial u}\Big{\|}_{t-1}$
	$\displaystyle\frac{\partial y_{t}}{\partial u_{t-2}}=$	$\displaystyle\frac{\partial g}{\partial x}\Big{\|}_{t}\frac{\partial f}{\partial x}\Big{\|}_{t-1}\frac{\partial f}{\partial u}\Big{\|}_{t-2}$
	$\displaystyle\frac{\partial y_{t}}{\partial u_{t-3}}=$	$\displaystyle\frac{\partial g}{\partial x}\Big{\|}_{t}\frac{\partial f}{\partial x}\Big{\|}_{t-1}\frac{\partial f}{\partial x}\Big{\|}_{t-2}\frac{\partial f}{\partial u}\Big{\|}_{t-3}$
	$\displaystyle\vdots\$

Therefore, it is clear that (45) provides an accurate and concise representation of these results. ∎

Under the agent dynamics model (1), the control input signal $u=\{u_{t}\}_{t\in[0,T]}$ and the state signal $x=\{x_{t}\}_{t\in[0,T]}$ are related such that, for all $t,\tau\in[0,T]$ ,

\frac{\partial x_{t}}{\partial u_{\tau}}=\begin{cases}\prod_{i=1}^{t-\tau-1}\left[\frac{\partial f}{\partial x}\Big{|}_{t-i}\right]\frac{\partial f}{\partial u}\Big{|}_{\tau},\ \ &\mbox{if }\tau<t,\\ 0,\ \ &\mbox{if }\tau\geq t.\\ \end{cases}

(47)

From the agent dynamics model (1), we can write

$\displaystyle x_{t}=$	$\displaystyle f(x_{t-1},u_{t-1})$	(48)
$\displaystyle=$	$\displaystyle f(f(x_{t-2},u_{t-2}),u_{t-1})$
$\displaystyle=$	$\displaystyle f(f(f(x_{t-3,u_{t-3}}),u_{t-2}),u_{t-1})$
$\displaystyle\vdots$

Hence, $\frac{\partial x_{t}}{\partial u_{\tau}}=0$ for any $\tau\geq t$ and $\frac{\partial x_{t}}{\partial u_{t-1}}=\frac{\partial f}{\partial u}\big{|}_{t-1}$ . Similarly, using (48) together with the product rule, we can write

	$\displaystyle\frac{\partial x_{t}}{\partial u_{t-2}}=$	$\displaystyle\frac{\partial f}{\partial x}\Big{\|}_{t-1}\frac{\partial f}{\partial u}\Big{\|}_{t-2}$
	$\displaystyle\frac{\partial x_{t}}{\partial u_{t-2}}=$	$\displaystyle\frac{\partial f}{\partial x}\Big{\|}_{t-1}\frac{\partial f}{\partial x}\Big{\|}_{t-2}\frac{\partial f}{\partial u}\Big{\|}_{t-3}$
	$\displaystyle\vdots\$

Therefore, it is clear that (47) provides an accurate and concise representation of these results. ∎

Using these two lemmas, we now propose a theorem that can be used to determine the required gradient term: $\frac{\partial s}{\partial u}$ .

Under the agent dynamics model (1), the gradient of the composite signal $s(u)$ with respect to the control signal $u$ is given by a $(T+1)\times(T+1)$ block matrix $\frac{\partial s}{\partial u}$ (as in (44)) with its $(t,\tau)$ ^th block being

\frac{\partial s_{t}}{\partial u_{\tau}}=\begin{bmatrix}\frac{\partial y_{t}}{\partial u_{\tau}}\\ \frac{\partial x_{t}}{\partial u_{\tau}}\\ I_{m}\end{bmatrix}\in\mathbb{R}^{q\times m}

(49)

where $\frac{\partial y_{t}}{\partial u_{\tau}}\in\mathbb{R}^{p\times m}$ is given by (45), $\frac{\partial x_{t}}{\partial u_{\tau}}\in\mathbb{R}^{n\times m}$ is given by (47) and $I_{m}$ is the identity matrix in $\mathbb{R}^{m\times m}$ .

This result directly follows from Lms. 8, 9 and the format of the composite signal $s(u)=\{s_{t}(u)\}_{t\in[0,T]}\in\mathbb{R}^{1\times(T+1)q}$ where $s_{t}(u)\triangleq[y_{t}^{\top}(u),x_{t}^{\top}(u),u_{t}^{\top}]^{\top}$ . ∎

With that, we now can explicitly evaluate the gradient of the used SRM: $\frac{\partial\tilde{\rho}^{\varphi}(s(u))}{\partial u}$ (i.e., the gradient of the objective function used in the synthesis problem (6)) using (41) and Theorems 2 and 3.

In this section, to highlight our contributions, we consider the four symbolic control problems (SCPs) shown in Fig. 1. In each SCP, the objective is to synthesize a control signal for a simple simulated robot that follows 2-D integrator dynamics [20] such that it satisfies a given specification (indicated in Fig. 1). We have implemented: 1) the SCPs shown in Fig. 1, 2) the SRMs discussed in Section III, 3) the STL error semantics proposed in Section IV and 4) the STL gradient semantics proposed in V, in a Python environment that has been made available at https://github.com/shiran27/Symbolic-Control-via-STL for reproduction and reuse purposes.

In order to solve the aforementioned synthesis problem (i.e., (6)) in an energy-aware manner, we follow the approach used in [20] where a smooth cost function

\tilde{J}(u)\triangleq\tilde{\rho}^{\varphi}(s(u))-0.01\|u\|^{2}

(50)

is optimized (as an alternative to optimizing its non-smooth version: $J(u)\triangleq\rho^{\varphi}(s(u))-0.01\|u\|^{2}$ , see also (7)), using the SciPy’s SQP method [27].

Refer to caption — (a) SCP1: The specification is $\varphi=\varphi_{o}\land\varphi_{u}\land\textbf{F}_{[0,20]}\mbox{Tar}1$ .

We start with illustrating the efficiency and the accuracy of the explicit gradient computation technique proposed in Section V. For this purpose, we compare such explicit gradients with the gradients provided by the symbolic AutoGrad software package [26] (that was used in [20]) - in terms of the execution times and the absolute component differences (errors). It is also worth noting that the said AutoGrad based approach is much more efficient and accurate compared to numerical methods where the gradient is computed using finite differences [21].

In our experiments, for each SCP shown in Fig. 1 and for each SRM, the explicit gradient and the AutoGrad based gradient (of the cost function) were evaluated at 500 randomly selected control signals. The observed mean execution times and the ( $\log$ ) mean absolute component errors are reported in Tab. III. According to the observed execution times, the proposed explicit gradient evaluation technique is significantly efficient compared to the AutoGrad based technique as it has improved the mean execution time on average by 57.7% irrespective of the considered SCP or the SRM. Moreover, the observed error values (in log scale) reveal that both gradient computing techniques essentially provide the same gradient values.

However, notice a considerable difference in the scale (albeit small in the magnitude) in the observed error values across different SRMs. Therefore, this behavior was further investigated under varying smooth operator parameters $k_{1},k_{2}$ , for the SCP3. The observed results are illustrated in Fig. 2. Intuitively, with increasing $k_{1}$ , $k_{2}$ values, an SRM becomes approximately close to the actual non-smooth robustness measure, and thus, the corresponding gradients evaluated using the AutoGrad method can be expected to deviate from the actual explicit gradients. However, according to the observations shown in Fig. 2, such a behavior can only be seen for SRM2 and SRM4. Moreover, error magnitudes associated with SRM3 and SRM1 are lower (mush significantly in the latter case) than those of SRM2 and SRM4. Hence, we can conclude that SRMs like SRM1 and SRM3 can be used even with the AutoGrad package (to compute gradients) without running into significant numerical inaccuracies irrespective of the used $k_{1}$ , $k_{2}$ values.

TABLE III: A comparison between explicit gradients and AutoGrad based gradients. Each SRM was defined using the smooth operator parameters

k_{1}=k_{2}=3

SCP

SRM

Mean Execution Time / (ms)

Absolute Component Error

Explicit

AutoGrad

% Impr.

\log_{10}(\text{Mean})

\log_{10}(\text{St.D.})

SRM1

23.3

54.9

57.6

-16.6

-16.4

SRM2

23.9

56.0

57.2

-16.1

-15.8

SRM3

24.8

56.6

56.3

-16.0

-15.8

SCP1

SRM4

25.6

57.0

55.2

-15.8

-15.5

SRM1

46.8

115.0

59.3

-16.2

-15.9

SRM2

44.1

105.8

58.3

-15.7

-15.3

SRM3

43.8

104.2

58.0

-15.6

-15.3

SCP2

SRM4

49.8

114.5

56.5

-15.4

-15.1

SRM1

24.0

58.9

59.3

-15.5

-15.1

SRM2

24.9

60.9

59.0

-13.9

-13.5

SRM3

26.3

63.0

58.3

-14.2

-13.7

SCP3

SRM4

27.3

64.9

57.9

-13.8

-13.5

SRM1

62.8

150.9

58.4

-15.7

-15.4

SRM2

66.9

156.1

57.2

-14.7

-14.3

SRM3

64.4

150.7

57.2

-14.5

-14.2

SCP4

SRM4

72.3

168.3

57.0

-14.4

-14.1

We now compare different control solutions obtained for each SCP shown in Fig. 1 under different SRMs discussed in Section III. Here we also provide the details of respective approximation error bounds revealed by the STL error semantics proposed in Section IV. As mentioned before, in each scenario, similar to [20], we obtain the control solution by optimizing the smooth cost function $\tilde{J}(u)$ (50) using the SciPy’s SQP method [27]. However, one key difference compared to [20] is that we now provide explicitly computed gradients (i.e., $\frac{\partial\tilde{J}(u)}{\partial u}$ ) to this SQP solver.

For the purpose of comparing different control solutions obtained for a SCP, we can directly use the performance metrics: 1) the approximation error bound width $U_{\theta}^{\varphi}(s(u))-L_{\theta}^{\varphi}(s(u))$ , 2) the control cost $0.01\|u\|^{2}$ , 3) the non-smooth (actual) robustness measure $\rho^{\varphi}(s(u))$ and 4) the non-smooth (total) cost function $J(u)$ . These performance metrics, along with a few other metrics (that cannot be used for such comparisons, e.g., the smooth robustness measure $\tilde{\rho}(s(u))$ ) that were observed are summarized in Tab. IV. It is important to point out that all the values provided in Tab. IV are average values computed over 50 realizations, where in each realization, the SQP solver was initialized with a randomly selected control solution.

According to the simulation results reported in Tab. IV, in each SCP, the control solution found using the SRM3 provides the best total cost function value and the best actual robustness value, while the control solution found using the SRM1 provides the best control cost and the best approximation error bound width. This behavior implies that: 1) using an SRM with a moderate-sized approximation error bound (like the SRM3, as opposed to the SRM1) can lead to control solutions with better actual robustness measures, and 2) different SRMs can favor different aspects of the composite cost function (e.g., SRM1 favors reducing the control cost while the SRM2 favors improving robustness measure). Moreover, based on the performance metrics considered in Tab. IV, notice that both SRM2 and SRM4 do not show noticeable results compared to SRM1 or SRM3. In fact, for the SCP4, on average, SRM2 and SRM4 fail to find a feasible solution (as $\rho^{\varphi}<0$ ).

To further investigate the properties of different SRMs, we executed the same set of experiments (that generated the results reported in Tab. IV) with different smooth operator parameter values: $k_{1},k_{2}\in\{1,3,5,7,9\}$ . The observed results (omitting some indecisive cases for simplicity) are summarized in Tab. V. Similar to before, these observations show that across different $k_{1},k_{2}$ values and SCPs, the SRM1 provides the best control cost and the best approximation error bound width (if it finds a feasible solution). Also, in terms of the actual robustness measure and the total cost function value, the SRM3 performs better than the SRM1 in 65% of the cases considered. Furthermore, the results in Tab. V show that: 1) the overall best robustness measure value achieved for each SCP has been achieved when using the SRM3, 2) the SRM3 is more effective (compared to the SRM1) with low $k_{1},k_{2}$ values, 3) the SRM3 finds a feasible solution irrespective of the $k_{1},k_{2}$ values used, 4) the SRM1 is more effective (compared to the SRM3) with high $k_{1},k_{2}$ values, and, 5) the SRM1 can fail to find a feasible solution when the used $k_{1},k_{2}$ values are small.

Naturally, the aforementioned conflicting properties among different SRMs encourage one to jointly use two (or more) SRMs to achieve better performance metrics. For example, a control solution obtained using the SRM3 can be applied to initialize a subsequent stage where the SRM1 will be used. In fact, when this exact strategy was applied to the considered four SCPs (with $k_{1}=k_{2}=3$ , as in Tab. IV), the percentage improvements achieved in terms of the average actual robustness measure were: 0.17%, 1.80%, 45.9% and 0.83%, respectively.

Another example approach (to jointly use two SRMs) is to constantly switch between using the SRM2 and the SRM3 while following a gradient ascent scheme that optimizes the smooth cost function (50). Recall that the SRM2 and the SRM3 are essentially under- and over-approximations to the actual robustness measure. Hence, as illustrated in Fig. 3, with a properly selected switching strategy, this approach will guarantee an approximation error bound width $(\tilde{\rho}^{\varphi}_{3}-\tilde{\rho}^{\varphi}_{2})$ , where $\tilde{\rho}^{\varphi}_{3}$ and $\tilde{\rho}^{\varphi}_{2}$ are the converged SRM2 and SRM3 values, respectively. For example, for the four considered SCPs (with $k_{1}=k_{2}=3$ ), if the reported SRM2 and SRM3 values in Tab. IV were assumed to be the converged respective SRM2 and SRM3 values under a switching-gradient-ascent approach (as in Fig. 3), the percentage improvements in the approximation error bound widths would be: 63.3%, 71.7%, 77.7% and 44.1%, respectively.

TABLE IV: A performance comparison of different control solutions observed under different SRMs. Each SRM was defined using the smooth operator parameters

k_{1}=k_{2}=3

. All the reported values are average values computed over 50 realizations.

Smooth

Error Bound Information

Non-Smooth

SCP

SRM

Cont.

Cost

\tilde{J}

Rob.

\tilde{\rho}^{\varphi}

L_{\theta}^{\varphi}

U_{\theta}^{\varphi}

Width

Rob.

\rho^{\varphi}

Cost

J

SCP1

SRM1

0.072

-0.810

-0.739

-1.025

1.853

2.878

0.182

0.110

SRM2

0.074

-0.847

-0.772

-0.010

4.245

4.255

0.338

0.264

SRM3

0.079

0.620

0.698

-3.982

0.010

3.992

0.401

0.323

SRM4

0.096

0.395

0.491

-3.373

4.419

7.792

0.152

0.057

SCP2

SRM1

0.093

-0.892

-0.799

-1.025

1.853

2.878

0.264

0.170

SRM2

0.100

-0.942

-0.843

-0.010

5.184

5.194

0.150

0.050

SRM3

0.102

0.528

0.630

-10.037

0.010

10.047

0.321

0.220

SRM4

0.116

0.352

0.468

-9.543

4.110

13.653

0.155

0.040

SCP3

SRM1

0.214

-0.416

-0.202

-0.703

1.853

2.556

0.524

0.310

SRM2

0.245

-0.522

-0.276

-0.010

6.266

6.276

0.523

0.278

SRM3

0.236

0.856

1.091

-6.176

0.010

6.186

0.620

0.385

SRM4

0.276

0.625

0.901

-5.359

3.823

9.182

0.463

0.187

SCP4

SRM1

0.231

-0.673

-0.442

-0.703

1.988

2.691

0.410

0.179

SRM2

0.167

-1.896

-1.729

-0.010

4.409

4.419

-1.345

-1.512

SRM3

0.242

0.574

0.816

-7.107

0.010

7.117

0.506

0.264

SRM4

0.147

-1.450

-1.303

-9.295

4.526

13.822

-1.535

-1.681

TABLE V: A performance comparison of different control solutions observed under SRM1 and SRM3 with varying smooth operator parameter values

k_{1},k_{2}\in\{1,3,5,7,9\}

. All the reported values are average values computed over 50 realizations.

SCP	SRM	Error Bound width: $U^{\varphi}_{\theta}(s(u))-L^{\varphi}_{\theta}(s(u))$					Control Cost: $0.01\\|u\\|^{2}$					Robustness Measure: $\rho^{\varphi}(s(u))$					Cost: $J(u)=\rho^{\varphi}(s(u))-0.01\\|u\\|^{2}$
		k_1=k_2					k_1=k_2					k_1 = k_2					k_1 = k_2
		1	3	5	7	9	1	3	5	7	9	1	3	5	7	9	1	3	5	7	9
SCP1	SRM1	8.594	2.878	1.735	1.245	\ul0.973	0.068	\ul0.072	0.072	0.073	0.073	-1.213	0.182	0.349	0.400	0.416	-1.281	0.110	0.277	0.327	\ul0.343
SCP1	SRM3	8.635	3.992	3.420	2.766	2.946	0.080	0.079	0.079	0.079	0.078	0.192	0.401	\ul0.416	0.401	0.399	0.112	0.323	0.338	0.323	0.320
SCP2	SRM1	8.594	2.878	1.735	1.245	\ul0.973	0.097	\ul0.093	0.094	0.094	0.093	-0.896	0.264	0.335	0.360	0.372	-0.993	0.170	0.241	0.266	\ul0.278
SCP2	SRM3	11.648	10.047	9.456	8.982	8.741	0.102	0.102	0.098	0.100	0.098	0.185	0.321	\ul0.372	0.360	0.346	0.083	0.220	0.274	0.260	0.248
SCP3	SRM1	7.629	2.556	1.542	1.107	\ul0.865	\ul0.118	0.214	0.225	0.223	0.219	0.187	0.524	0.602	0.596	0.590	0.069	0.310	0.376	0.374	0.371
SCP3	SRM3	7.251	6.186	5.498	5.105	5.179	0.165	0.236	0.248	0.235	0.226	0.542	\ul0.620	0.568	0.590	0.574	0.376	\ul0.385	0.320	0.355	0.348
SCP4	SRM1	8.034	2.691	1.623	1.165	\ul0.910	0.227	0.231	0.229	0.222	0.219	0.061	0.410	0.506	0.512	0.524	-0.166	0.179	0.276	0.290	0.304
SCP4	SRM3	8.866	7.117	6.451	6.348	6.021	0.231	0.242	0.235	\ul0.217	0.220	0.151	0.506	0.494	0.532	\ul0.538	-0.080	0.264	0.258	0.315	\ul0.317

We finally highlight three possible interesting uses of approximation error bounds determined by the STL error semantics proposed in Section IV. Before getting into the details, recall the notation that we used to represent an approximation error bound: $[L_{\theta}^{\varphi},U_{\theta}^{\varphi}]\ni\tilde{e}^{\varphi}(s(u))\triangleq(\rho^{\varphi}(s(u))-\tilde{\rho}^{\varphi}(s(u))\})$ and the fact that we optimize a SRM $\tilde{\rho}^{\varphi}(s(u))$ using a gradient-based optimization process.

The first use of knowing the error bound $[L_{\theta}^{\varphi},U_{\theta}^{\varphi}]$ is that it allows one to terminate the said optimization process prematurely if a given minimum level of actual robustness $\rho^{\varphi}(s(u))$ is guaranteed to be achieved. For example, if we need to ensure $\rho^{\varphi}(s(u))>L$ for some known $L\in\mathbb{R}$ value, we can use the simple (also efficient and smooth) termination condition: $\tilde{\rho}^{\varphi}(s(u))\geq L-L_{\theta}^{\varphi}$ in the gradient-based optimization process. As a numerical example, consider the (average) case for the SCP1 with the SRM2 reported in Tab. IV and assume we need to ensure $\rho^{\varphi}(s(u))>-1$ . By simply looking at the achieved $\tilde{\rho}^{\varphi}(s(u))$ and $L_{\theta}^{\varphi}$ values, one can directly conclude that $\rho^{\varphi}(s(u))>-1$ as $\tilde{\rho}^{\varphi}(s(u))=-0.772\geq L-L_{\theta}^{\varphi}=-1-(-0.01)=-0.99$ .

The next use of error bounds is that it allows one to see how uncertainties in the mission space translate into uncertainties in the actual robustness measure. For example, in Tab. IV, under any SCP, notice that $L^{\varphi}_{\theta}=-0.01$ in SRM2 and $U^{\varphi}_{\theta}=0.01$ in SRM3 (even though, they both should be zero according to Lms. 3 and 5, respectively). This is because, in our experiments, we have assumed that each predicate value (i.e., $\mu^{\pi}(s_{t})$ ) can be deviated by $\pm 0.01$ from its true value due to some source of noise. In other words, we set $L^{\pi}(s_{t})=L^{\pi}=-0.01$ and $U^{\pi}(s_{t})=U^{\pi}=0.01$ for all $s_{t}$ and $\pi$ , in the experiments (see also (33)). In applications, since these $L^{\pi}$ and $U^{\pi}$ values can take different values depending on the predicate $\pi$ , it is far from obvious that how such terms will determine an accuracy error bound: $[L^{\varphi},U^{\varphi}]\ni\hat{e}^{\varphi}(s(u))\triangleq(\rho^{\varphi}(s(u))-\hat{\rho}^{\varphi}(s(u)))$ , where $\hat{\rho}^{\varphi}(s(u))$ is the computed/estimated actual robustness measure and $\rho^{\varphi}(s(u))$ is the true actual robustness measure. However, note that we now can address this challenge by simply using the supplementary STL error semantics proposed in Def. 5 with $L_{k_{1},m}^{\min}=U_{k_{1},m}^{\min}=L_{k_{2},m}^{\min}=U_{k_{2},m}^{\min}=0$ to compute the said accuracy error bound $[L^{\varphi},U^{\varphi}]$ .

Finally, we elaborate on the main intended use of the proposed error bound analysis, i.e., to select (tune) the smooth operator parameters $\theta=\{k_{1},k_{2},...\}$ . Intuitively, for this purpose, one can solve an optimization problem of the form:

\theta^{*}=\underset{\theta>0}{\arg\min}\ \ (U^{\varphi}_{\theta}-L^{\varphi}_{\theta})+\alpha\theta^{T}\theta,

(51)

where $\alpha$ is a scaling factor and the second term in the RHS is a regulatory term that ensures the parameters in $\theta$ will not grow indefinitely. Note that this latter term is required because the error bound width $(U^{\varphi}_{\theta}-L^{\varphi}_{\theta})$ term in (51) converges to zero as the parameters in $\theta$ grow (irrespective of the used SRM). Clearly, with respect to the optimization process of the cost function (50), this parameter tuning stage (51) can be executed either off-line or on-line. A situation where off-line parameter tuning has lead to an improved solution is shown in Fig. LABEL:Fig:OfflineTuning. Further, Fig. 5 shows a case where on-line parameter tuning has been used - while the cost function (50) is being optimized using a gradient ascent process. From these motivating results, the importance of the proposed error bound analysis is evident. The future work is directed towards studying efficient and accurate ways to solve this parameter tuning problem (51) and investigating effective ways to combine it with the main optimization problem where the cost function (50) is optimized.

In this paper, we motivated the use of smooth robustness measures and gradient-based optimization methods to efficiently solve complex symbolic control problems where the specifications are given using Signal Temporal Logic. First, two existing and two new smooth robustness measures were extensively discussed while establishing their fundamental properties. Then, to characterize the approximation errors associated with different SRMs, we proposed a set of semantic rules that we named STL error semantics. This error analysis, among its other uses, enables one to assess different SRMs and sensibly select SRM parameters. Finally, to efficiently and accurately compute the gradients of different SRMs, we proposed another set of semantic rules that we named STL gradient semantics. Simulation results are provided to highlight the improvements achieved due to these contributions. Ongoing work aims to determine effective ways to use multiple SRMs in gradient-based optimization schemes simultaneously.

[1] A. Pnueli, “The Temporal Logic of Programs,” in Proc of Annual IEEE Symposium on Foundations of Computer Science, vol. 1977-October, 1977, pp. 46–57.
[2] E. M. Clarke and E. A. Emerson, “Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic,” in Logics of Programs, 1982, pp. 52–71.
[3] R. L. Schwartz, P. M. Melliar-Smith, and F. H. Vogt, “An Interval Logic for Higher-Level Temporal Reasoning,” in Proc. of 2nd Annual ACM Symposium on Principles of Distributed Computing. New York, New York, USA: ACM Press, 1983, pp. 173–186.
[4] R. Koymans, “Specifying Real-Time Properties with Metric Temporal Logic,” Real-Time Systems, vol. 2, no. 4, pp. 255–299, 1990.
[5] C. I. Vasile, D. Aksaray, and C. Belta, “Time Window Temporal Logic,” Theoretical Computer Science, vol. 691, pp. 27–54, 2017.
[6] O. Maler and D. Nickovic, “Monitoring Temporal Properties of Continuous Signals,” Lecture Notes in Computer Science, vol. 3253, pp. 152–166, 2004.
[7] N. Mehdipour, C. I. Vasile, and C. Belta, “Arithmetic-Geometric Mean Robustness for Control From Signal Temporal Logic Specifications,” in Proc. of American Control Conf., vol. 2019-July, 2019, pp. 1690–1695.
[8] I. Haghighi, N. Mehdipour, E. Bartocci, and C. Belta, “Control from Signal Temporal Logic Specifications with Smooth Cumulative Quantitative Semantics,” in Proc. of 58th IEEE Conf. on Decision and Control, vol. 2019-Decem, 2019, pp. 4361–4366.
[9] Y. V. Pant, H. Abbas, R. A. Quaye, and R. Mangharam, “Fly-by-Logic: Control of Multi-Drone Fleets with Temporal Logic Objectives,” in Proc. of 9th ACM/IEEE Intl. Conf. on Cyber-Physical Systems, 2018, pp. 186–197.
[10] G. E. Fainekos, S. Sankaranarayanan, K. Ueda, and H. Yazarel, “Verification of Automotive Control Applications Using S-TaLiRo,” in Proc. of American Control Conf., 2012, pp. 3567–3572.
[11] V. Raman, A. Donzé, D. Sadigh, R. M. Murray, and S. A. Seshia, “Reactive Synthesis from Signal Temporal Logic Specifications,” in Proc. of 18th Intl. Conf. on Hybrid Systems: Computation and Control, 2015, pp. 239–248.
[12] S. Sankaranarayanan and G. Fainekos, “Simulating Insulin Infusion Pump Risks by In-Silico Modeling of the Insulin-Glucose Regulatory System,” in Proc. of Intl. Conf. on Computational Methods in Systems Biology, 2012, pp. 322–341.
[13] N. Mehdipour, D. Briers, I. Haghighi, C. M. Glen, M. L. Kemp, and C. Belta, “Spatial-Temporal Pattern Synthesis in a Network of Locally Interacting Cells,” in Proc. of 58th IEEE Conf. on Decision and Control, vol. 2018-Decem, 2019, pp. 3516–3521.
[14] C. Belta and S. Sadraddini, “Formal Methods for Control Synthesis: An Optimization Perspective,” Annual Review of Control, Robotics, and Autonomous Systems, vol. 2, no. 1, pp. 115–140, 2019.
[15] S. Saha and A. A. Julius, “An MILP Approach for Real-Time Optimal Controller Synthesis with Metric Temporal Logic Specifications,” in Proc. of the American Control Conf., vol. 2016-July, 2016, pp. 1105–1110.
[16] H. Abbas and G. Fainekos, “Convergence Proofs for Simulated Annealing Falsification of Safety Properties,” in Proc. of 50th Annual Allerton Conference on Communication, Control, and Computing, 2012, pp. 1594–1601.
[17] S. M. LaValle and J. James J. Kuffner, “Randomized Kinodynamic Planning,” The International Journal of Robotics Research, vol. 20, no. 5, pp. 378–400, 2001.
[18] H. Abbas and G. Fainekos, “Computing Descent Direction of MTL Robustness for Non-Linear Systems,” in Proc. of American Control Conf., 2013, pp. 4405–4410.
[19] H. Abbas, A. Winn, G. Fainekos, and A. A. Julius, “Functional Gradient Descent Method for Metric Temporal Logic Specifications,” in Proc. of American Control Conference, 2014, pp. 2312–2317.
[20] Y. Gilpin, V. Kurtz, and H. Lin, “A Smooth Robustness Measure of Signal Temporal Logic for Symbolic Control,” IEEE Control Systems Letters, vol. 5, no. 1, pp. 241–246, 2021.
[21] Y. V. Pant, H. Abbas, and R. Mangharam, “Smooth Operator: Control Using the Smooth Robustness of Temporal Logic,” in Proc. of 1st IEEE Conf. on Control Technology and Applications, vol. 2017-Janua, 2017, pp. 1235–1240.
[22] L. Lasdon and J. C. Plummer, “Multistart algorithms for seeking feasibility,” Computers and Operations Research, vol. 35, no. 5, pp. 1379–1393, may 2008.
[23] S. Welikala and C. G. Cassandras, “Distributed Non-Convex Optimization of Multi-Agent Systems Using Boosting Functions to Escape Local Optima,” IEEE Trans. on Automatic Control, 2020.
[24] H. H. Hoos and T. Stutzle, “Praise for Stochastic Local Search: Foundations and Applications,” in Stochastic Local Search. Morgan Kaufmann Publishers, 2005, pp. i–ii.
[25] M. Lange, D. Zühlke, O. Holz, and T. Villmann, “Applications of lp-Norms and Their Smooth Approximations for Gradient Based Learning Vector Quantization,” in Proc. of European Symposium on Artificial Neural Networks, 2014, pp. 271–276.
[26] D. Maclaurin, D. Duvenaud, and R. P. Adams, “Autograd: Effortless Gradients in numpy,” in Proc. of ICML AutoML Workshop, 2015, pp. 1–3.
[27] P. Virtanen, R. Gommers, T. E. Oliphant, M. Haberland, T. Reddy, D. Cournapeau, E. Burovski, P. Peterson, W. Weckesser, J. Bright, S. J. van der Walt, M. Brett, J. Wilson, K. J. Millman, N. Mayorov, A. R. J. Nelson, E. Jones, R. Kern, E. Larson, C. J. Carey, I. Polat, Y. Feng, E. W. Moore, J. VanderPlas, D. Laxalde, J. Perktold, R. Cimrman, I. Henriksen, E. A. Quintero, C. R. Harris, A. M. Archibald, A. H. Ribeiro, F. Pedregosa, and P. van Mulbregt, “SciPy 1.0: Fundamental Algorithms for Scientific Computing in Python,” Nature Methods, vol. 17, no. 3, pp. 261–272, 2020. [Online]. Available: https://www.nature.com/articles/s41592-019-0686-2

$\displaystyle u^{*}=$

$\displaystyle\ \underset{u}{\arg\max}$

$\displaystyle\rho^{\varphi_{0}}((y,0))$

Subject to:

$\displaystyle x_{t+1}=f(x_{t},u_{t}),\ x_{0}\mbox{ is a given,}$

$\displaystyle y_{t}=g(x_{t},u_{t}),$

$\displaystyle y_{t}\in\mathcal{Y},\ x_{t}\in\mathcal{X},\ u_{t}\in\mathcal{U},\ \forall t\in[0,T].$