Arithmetic-Geometric Mean Robustness for Control from Signal Temporal Logic Specifications

TL;DR

This paper introduces an average-based robustness score for Signal Temporal Logic (STL) that emphasizes the frequency and robustness of specification satisfaction, improving control and monitoring of dynamical systems.

Contribution

It proposes a novel arithmetic-geometric mean robustness measure for STL and a framework for optimal control under STL constraints, enhancing satisfaction assessment.

Findings

The new robustness score better reflects satisfaction quality.

Framework effectively guides control synthesis.

Case studies demonstrate practical advantages.

Abstract

We present a new average-based robustness score for Signal Temporal Logic (STL) and a framework for optimal control of a dynamical system under STL constraints. By averaging the scores of different specifications or subformulae at different time points, our new definition highlights the frequency of satisfaction, as well as how robustly each specification is satisfied at each time point. We show that this definition provides a better score for how well a specification is satisfied. Its usefulness in monitoring and control synthesis problems is illustrated through case studies.

Equations

$$\phi :=\top \mid \mu \mid \neg \phi \mid {\phi }_1\wedge {\phi }_2\mid {\phi }_1{\mathbf{U}}_{[a,b]}{\phi }_2,$$

$$\rho (\top ,S,t)$$

$$\rho (\perp ,S,t)$$

$$\rho (\mu ,S,t)$$

$$\rho \left(\neg \phi ,S,t\right)$$

$$\rho \left({\phi }_1\wedge {\phi }_2,S,t\right)$$

$$\rho \left({\phi }_1\vee {\phi }_2,S,t\right)$$

$$\rho \left({\mathbf{G}}_{[a,b]}\phi ,S,t\right)$$

$$\rho \left({\mathbf{F}}_{[a,b]}\phi ,S,t\right)$$

$$\begin{array}[]{l}{\max_{\beta}}(a_{1},\ldots,a_{m})\approx\frac{1}{\beta}\ln\sum_{i=1}^{m}e^{\beta a_{i}},\\ {\min_{\beta}}(a_{1},\ldots,a_{m})\approx-\frac{1}{\beta}\ln\sum_{i=1}^{m}e^{-\beta a_{i}}.\end{array}$$

$$\begin{array}[]{l}q[k+1]=f(q[k],u[k]),\\ q[0]=q_{0},\end{array}$$

$$\begin{array}[]{c}u^{*}=\mathop{\mathrm{argmin}}_{u}\sum\limits_{k=0}^{T-1}J(u[k],q[k+1]),\\ \text{s.t.}\;\;\;\;\;\langle q,{u}\rangle\models\phi.\\ \end{array}$$

$$\eta (\top ,S,t)$$

$$\eta (\perp ,S,t)$$

$$\eta (\phi ,S,t)$$

$$\eta (\neg \phi ,S,t)$$

$$\begin{array}[]{l}\eta({\varphi_{1}}\land...\land{\varphi_{m}},S,t\mid\forall i\in[1,...,m]\;.\;\eta({\varphi_{i}},S,t)>0):=\sqrt[m]{{\prod\limits_{i=1,...,m}{\left({1+\eta({\varphi_{i}},S,t)}\right)}}}-1\\ \\ \eta({\varphi_{1}}\lor...\lor{\varphi_{m}},S,t\mid\exists i\in[1,...,m]\ .\ \eta({\varphi}_{i},S,t)>0):=\frac{1}{m}\sum\limits_{i=1,...,m}[\eta(\varphi_{i},S,t)]_{+}\\ \\ \eta({{\mathbf{G}}_{[a,b]}}\varphi,S,t\mid\forall t_{k}^{\prime}\in[t+a,t+b]\ .\ \eta({\varphi},S,t_{k}^{\prime})>0):=\sqrt[N]{{\prod\limits_{t_{k}^{\prime}\in[t+a,t+b]}{\left({1+\eta(\varphi,S,t_{k}^{\prime})}\right)}}}-1\\ \\ \eta({{\mathbf{F}}_{[a,b]}}\varphi,S,t\mid\exists t_{k}^{\prime}\in[t+a,t+b]\ .\ \eta({\varphi},S,t_{k}^{\prime})>0):=\frac{1}{N}\sum\limits_{t_{k}^{\prime}\in[t+a,t+b]}[\eta(\varphi,S,t_{k}^{\prime})]_{+}\end{array}$$

$$\begin{array}[]{l}\eta({\varphi_{1}}\land...\land{\varphi_{m}},S,t\mid\exists i\in[1,...,m]\ .\ \eta({\varphi}_{i},S,t)\leq 0):=\frac{1}{m}\sum\limits_{i=1,...,m}[\eta(\varphi_{i},S,t)]_{-}\\ \\ \eta(\varphi_{1}\lor...\lor\varphi_{m},S,t\mid\forall i\in[1,...,m]\;.\;\eta({\varphi_{i}},S,t)\leq 0):=-\sqrt[m]{{\prod\limits_{i=1,...,m}{\left({1-\eta({\varphi_{i}},S,t)}\right)}}}+1\\ \\ \eta(\mathbf{G}_{[a,b]}\varphi,S,t\mid\exists t_{k}^{\prime}\in[t+a,t+b]\ .\ \eta({\varphi},S,t_{k}^{\prime})\leq 0):=\frac{1}{N}\sum\limits_{t_{k}^{\prime}\in[t+a,t+b]}[\eta(\varphi,S,t_{k}^{\prime})]_{-}\\ \\ \eta(\mathbf{F}_{[a,b]}\varphi,S,t\mid\forall t_{k}^{\prime}\in[t+a,t+b]\ .\ \eta({\varphi},S,t_{k}^{\prime})\leq 0):=-\sqrt[N]{{\prod\limits_{t_{k}^{\prime}\in[t+a,t+b]}{\left({1-\eta(\varphi,S,t_{k}^{\prime})}\right)}}}+1\end{array}$$

$$\eta (\phi ,S,t)>0\iff \rho (\phi ,S,t)>0\Rightarrow S\models \phi ,$$

$$\eta (\phi ,S,t)<0\iff \rho (\phi ,S,t)<0\Rightarrow S/\models \phi .$$

$$△(x,y)=\{\begin{array}{ll}\sqrt{(1+x)(1+y)}-1& x>0,y>0\\ \frac{[x{]}_{-}+[y{]}_{-}}{2}& \text{else}\end{array}$$

$$△(x,y)=△(y,x)$$

$$△(x,y)\le △(u,v),\forall x\le u,y\le v$$

$$△(x,x)=x$$

$$\begin{array}[]{l}\varphi_{1}=x_{robot}>5,\\ \varphi_{2}=\textit{Battery}>30,\\ \phi=\varphi_{1}\wedge\varphi_{2},\end{array}$$

$$\begin{array}[]{c}u^{*}=\mathop{\mathrm{argmax}}_{u}\eta(\phi,\langle q,u\rangle)\\ \;\text{s.t.}\;\;\;\;\;\eta(\phi,\langle q,u\rangle)>0.\end{array}$$

$$x^{i+1}\leftarrow x^i+{\alpha }^i\nabla F,$$

$$\begin{array}[]{c}u^{*}={\mathop{\mathrm{argmax}}}_{u}(\eta(\phi,\langle q,u\rangle)-\lambda\sum\limits_{k=0}^{T-1}J(u[k],q[k+1])),\\ \text{s.t.}\;\;\;\;\eta(\phi,\langle q,u\rangle)>0,\\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;q[k+1]=f(q[k],u[k]),\\ q[0]=q_{0},\\ q[k]\in\mathbf{Q}\subseteq\mathbb{R}^{n},\\ u[k]\in\mathbf{U}\subseteq\mathbb{R}^{m},\end{array}$$

$$\begin{array}[]{l}x[k+1]=x[k]+\cos\theta[k]v[k],\\ y[k+1]=y[k]+\sin\theta[k]v[k],\\ \theta[k+1]=\theta[k]+w[k],\\ \end{array}$$

$$\begin{array}[]{l}\phi_{1}=(\mathbf{G}_{[1,5]}\;\textit{Init})\wedge\;(\mathbf{F}_{[6,10]}\;\textit{Reg1})\\ \;\;\;\;\;\;\;\;\wedge\;(\mathbf{F}_{[11,15]}\;\textit{Reg2})\;\wedge(\mathbf{G}_{[0,15]}\;\neg\textit{Obs}),\end{array}$$

$$\begin{array}[]{l}q^{\prime}[k+1]=q^{\prime}[k]+q^{\prime}_{d}[k],\\ q^{\prime}_{d}[k+1]=q^{\prime}_{d}[k]+u_{q^{\prime}}[k],\end{array}$$

$$\begin{array}[]{l}x[k+1]=x[k]+\cos\theta[k]v[k],\\ y[k+1]=y[k]+\sin\theta[k]v[k],\\ \theta[k+1]=\theta[k]+v[k]w[k],\\ \end{array}$$

$$\begin{array}[]{l}\phi_{2}=(\mathbf{F}_{[1,5]}\;(\textit{Reg1}\vee\textit{Reg2}))\;\wedge(\mathbf{F}_{[6,10]}\textit{ Reg3})\\ \;\;\;\;\;\;\;\;\;\;\;\wedge\;(\mathbf{G}_{[0,10]}\;\neg\textit{Obs}),\end{array}$$

$$\begin{array}[]{l}x[k+1]=x[k]+u_{x}[k],\\ y[k+1]=y[k]+u_{y}[k],\end{array}$$

$${\varphi }_3=({\mathbf{F}}_{[1,5]}\text{Reg1})\wedge ({\mathbf{F}}_{[6,10]}\text{Reg2}),$$

$$\begin{array}[]{l}u_{\tilde{\rho}}^{*}\leftarrow u_{\tilde{\rho}}^{*}+\mathcal{{N}}(0,\sigma^{2}),\\ u_{\eta}^{*}\leftarrow u_{\eta}^{*}+\mathcal{{N}}(0,\sigma^{2})\end{array}$$

Full text

I INTRODUCTION

Formal methods have been recently used to express system behavior under complex temporal requirements, verify whether the system execution meets the desired requirements, or control the system to satisfy desirable specifications [1]. Temporal Logics including Linear Temporal Logics (LTL) [2], Metric Temporal Logic (MTL) [3], Signal Temporal Logic (STL) [4] and Time Window Temporal Logic (TWTL) [5] allow precise description of system properties over time. STL is equipped with qualitative and quantitative semantics, meaning that it not only can assess whether the system execution meets the desired requirements but also provides a measure of how well requirements are met, also known as robustness. As a result, STL has been widely used for many control purposes including path planning and motion planning [6], [7] or synthesis problems [8]. Higher robustness score shows a stronger satisfaction of the desired specifications. Therefore, it is desirable to maximize the robustness score in order to improve system behavior to satisfy desired temporal specifications.

The traditional robustness score introduced in [9] is non-convex and non-differentiable; therefore, it is not possible to use powerful optimization techniques to maximize it. Previous works for control under STL constraints focused on using heuristic algorithms or encoding constraints as Mixed Integer Linear Programming (MILP). Heuristic optimization approaches such as Particle Swarm Optimization, Simulated Annealing and Rapidly Exploring Random Trees (RRTs) were used for synthesis, falsification and control problems [10], [11], [12]. Heuristic approaches do not require a smooth objective function; however, these algorithms do not always provide a guarantee to find the optima and have many user-defined parameters that need to be set in advance.

Encoding temporal logic specifications as linear and boolean constraints was studied in [13], [14] and MILP optimization solvers such as Gurobi were used to solve the control synthesis problem. The most critical issue with MILPs is that they do not scale well as the number of variables increases, resulting in a NP-complete problem. For instance, to encode the temporal operator $eventually$ as MILP constraints, we need to add integer (binary) variables for each time point in the specified interval. Therefore, this approach could fail when solving problems with many variables or complex temporal constraints. Moreover, MILP implementations require all constraints (including the system dynamics in the control problem) to be linear. As a result, nonlinear dynamics must be linearized, if linearizable, which involves approximation.

Recently, there have been efforts to smooth the robustness function (score) in order to use gradient-based optimization algorithms. In [15], [16], the authors used smooth approximations of maximum and minimum functions to define a smooth robustness score in order to solve a control problem. Even though these works solved the non-differentiability issue, the resulting smooth approximation had errors compared to the traditional robustness. Therefore, positive robustness did not necessarily mean satisfaction of the specification unless it was greater than a pre-defined threshold.

The main drawback of these works is that traditional robustness is defined by the most critical point (most satisfaction or most violation). In [17], authors defined average STL robustness for continuous-time signals and defined positive and negative robustness to solve a falsification problem. Authors in [18] described MTL as linear time-invariant filters and used the average robustness for monitoring purposes. [19] improved robustness for discrete signals by defining Discrete Average Space Robustness, and removed its nonsmoothness by approximating to a simplified version. These works refined robustness score only for temporal operators while using traditional maximum and minimum functions for other operators.

Our main contribution of this paper is proposing a new average-based robustness score, which we call Arithmetic-Geometric Mean (AGM) robustness. This new quantitative semantics uses arithmetic and geometric means to take into account the robustness degrees for all the subformulae and at every time point in the horizon, and not just the most satisfying or violating ones. As a result, our robustness definition rewards policies that satisfy the requirements at more time steps and with higher scores. We show that this novel robustness definition provides a better margin in which the specification is still satisfied when external disturbances or system perturbations exist. Moreover, our normalized signed robustness degree provides a meaningful comparison when specifications involve requirements over signals with different scales. The advantages of our new definition in both monitoring and control problems are illustrated through case studies through the paper. We compare our results with those obtained using MILPs and smooth approximation methods.

II PRELIMINARIES

Let $f:\mathbb{R}^{n}\rightarrow\mathbb{R}$ be a real function. We define $[f]_{+}={\small\begin{cases}f&f>0\\ 0&\text{otherwise}\end{cases}}$ and $[f]_{-}=-[-f]_{+}$, where $f=[f]_{+}+[f]_{-}$.

II-A Signal Temporal Logics (STL)

STL was introduced in [4] to monitor temporal properties of real-valued signals. Consider a discrete time sequence $\tau:=\{t_{k}|k\in\mathbb{Z}_{\geq 0}\}$. A signal $S$ is a function $S:\tau\rightarrow\mathbb{R}^{n}$ that maps each time point $t_{k}\in\tau$ to an $n$-dimensional vector of real values $S[t_{k}]$, with $s_{i}$ being its $i$th component. Assume $[a,b]$ is the set of all $t_{k}\in\tau$ starting from $a$ up to $b$, with $a,b\in\tau;\;b>a\geq 0$. STL Syntax is defined as:

[TABLE]

where $\top$ is the logical True, $\mu$ is a predicate, $\lnot$, $\land$ are the Boolean negation and conjunction operators, respectively, and $\mathbf{U}$ is the temporal until operator. Logical False is $\bot:=\lnot\top$. Other Boolean and temporal operators are defined as $\varphi_{1}\lor\varphi_{2}:=\lnot(\lnot\varphi_{1}\land\lnot\varphi_{2})$, $\mathbf{F}_{[a,b]}\varphi:=\top\mathbf{U}_{[a,b]}\varphi$, $\mathbf{G}_{[a,b]}\varphi:=\lnot\mathbf{F}_{[a,b]}\lnot\varphi$. In this paper, we focus on $\mathbf{F}$ and $\mathbf{G}$ operators, rather than $\mathbf{U}$. The temporal operator Finally or eventually ($\mathbf{F}_{[a,b]}\varphi$) states that “at some time point in $[a,b]$ the specification $\varphi$ must be True”; while globally or always ($\mathbf{G}_{[a,b]}\varphi$) states that “$\varphi$ must be True at all times in $[a,b]$”. The until operator ($\varphi_{1}\mathbf{U}_{[a,b]}\varphi_{2}$) states that “$\varphi_{2}$ must become True at some time point within $[a,b]$ and $\varphi_{1}$ must be always True prior to that”. A specification written in STL consists of predicates $\mu:=l(S)\geq 0$, where $l:\mathbb{R}^{n}\to\mathbb{R}$ is a real, possibly nonlinear, function defined over values of elements of $S$ (for instance, $s_{1}^{3}+s_{2}^{2}-2\geq 0$ or $-2s_{2}+10\geq 0$) connected by Boolean and temporal operators.

The STL qualitative semantics shows whether a signal $S$ satisfies a given specification $\varphi$ at time $t$, i.e., $S[t]\models\varphi$ or not, i.e., $S[t]\nmodels\varphi$, and its quantitative semantics, also known as robustness, measures how much the signal is satisfying or violating the specification.

Definition 1** (STL Robustness)**

Given a specification $\varphi$ and a signal $S$, the robustness score $\rho(\varphi,S,t)$ at time $t$ is recursively computed as [9]:

[TABLE]

where $\rho_{\top}\in\mathbb{R}\cup\{+\infty\}$ is the maximum robustness.

Theorem 1

The robustness score is sound, meaning that $\rho\left({\varphi,S,t}\right)>0$ implies that signal $S$ satisfies $\varphi$ at time $t$, and $\rho\left({\varphi,S,t}\right)<0$ implies that $S$ violates $\varphi$ at time $t$.

We denote the robustness score of specification $\varphi$ at time [math] with respect to the signal $S$ by $\rho(\varphi,S)$. We refer to this definition as traditional robustness score.

II-B $\min$/$\max$ Approximation

The $\min$ and $\max$ functions in the robustness definition in (2) result in a non-differentiable robustness score. This non-differentiability can be removed by replacing $\max$ and $\min$ functions with the following smooth approximations:

[TABLE]

For different values of $\beta$ different robustness scores are found, resulting in an error. It is shown in [16] that the approximation error approaches [math] as $\beta$ goes to $\infty$. We refer to this definition as approximation robustness score $\tilde{\rho}$.

III PROBLEM STATEMENT

Consider a discrete-time dynamical system given by:

[TABLE]

where $q[k]\in\mathbf{Q}\subseteq\mathbb{R}^{n}$ is the state of the system and $u[k]\in\mathbf{U}\subseteq\mathbb{R}^{m}$ is the control input at the $k$th time step $k\in\mathbb{Z}_{\geq 0}$; $q_{0}\in\mathbf{Q}$ is the initial state and $f$ is a function representing the dynamics of the system. Given the initial state $q_{0}$ and control sequence $u=\{u[0]u[1]...\}$, system trajectory $q=\{q[0]q[1]q[2]...\}$ is generated using (4); which we denote by $\langle q,u\rangle$. Consider a cost function $J(u[k],q[k+1])$ representing the cost of applying the control input $u[k]$. Assume system temporal requirements are given by a STL formula $\phi$ with a time horizon $T$, which is the largest time step for which signal values are needed in order to compute the robustness for the current time point. The control synthesis problem can be formulated as determining a control policy $u^{*}=\{u^{*}[0]u^{*}[1]...u^{*}[T-1]\}$ such that the system trajectory satisfies the STL specification $\phi$ while optimizing the cost:

[TABLE]

As stated in the Sec. I, previous works used heuristic algorithms, MILP encoding, and gradient ascent to solve (5) and found control policies to generate trajectories that satisfy STL constraints with the traditional and smooth robustness definition. The main shortcoming of the traditional robustness score is that it only considers the robustness of the most satisfying or violating part of the specification without taking into account satisfaction of the other parts. We address this limitation by defining a new version of robustness.

IV ARITHMETIC-GEOMETRIC MEAN (AGM) ROBUSTNESS

We define a novel robustness score $\eta$ based on arithmetic and geometric means instead of the $\max$ and $\min$ functions in the traditional definition. We show that our normalized signed robustness score $\eta\in[-1,1]$ provides a better understanding of system properties, where $\eta\in(0,1]$ corresponds to satisfaction of the specification, $\eta\in[-1,0)$ shows violation, and $\eta=0$ indicates inconclusiveness. Moreover, $|\eta|$ is a measure of how well the specification is satisfied or violated.

Consider a discrete time series $\tau:=\{t_{k}|k\in\mathbb{Z}_{\geq 0}\}$. Signal $S$ is a function $S:\tau\rightarrow\mathbb{R}^{n}$ that maps each time point $t_{k}\in\tau$ to an $n$-dimensional vector of real values $S[t_{k}]$, with $s_{i}$ being its $i$th element. Throughout the definitions and proofs, we assume that we have bounded signals, and all their components are normalized to the interval $[-1,1]$.

Definition 2** (AGM Robustness)**

Let $S:\tau\to{[-1,1]}^{n}$ and $\varphi:s_{i}-\pi\geq 0$ where $\pi\in[-1,1]$. The normalized signed AGM robustness $\eta(\varphi,S,t)$ with respect to the signal $S$ at time $t$ is defined as:

[TABLE]

For combination of other boolean and temporal operators in a time interval $[a,b]$, AGM robustness is recursively defined using (7) and (8); with $[a,b]=\{t_{k}|t_{k},a,b\in\tau;a\leq t_{k}\leq b;\;\;b>a\geq 0\}$ and $N$ being the number of time points in $[a,b]$.

Same as before, when the time of satisfaction is not mentioned, satisfaction at time [math] is considered, i.e., $\eta(\varphi,S)=\eta(\varphi,S,0)$. We first find robustness for each individual subformula using (6). Algorithm 1, Algorithm 2, Algorithm 3 and Algorithm 4 then determine satisfaction or violation of the specification with respect to the signal $S$ as well as the normalized signed AGM robustness score.

Remark 1

The command $ANY$ used in the AGM robustness algorithms is employed to check satisfaction or violation of the specification and determine the resulting robustness score, for which the worst case complexity is ${\rm O}(n)$.

Theorem 2** (Soundness)**

The AGM robustness score is sound, meaning that a satisfying trajectory has a strictly positive robustness:

[TABLE]

Proof:

We prove the property by structural induction over the formula $\varphi$. The base case corresponding to $\varphi\in\{\top,\bot,\mu\}$ is trivially true by definition from (6).

Let S be a signal. We have the following induction cases:

Negation: Let $\phi=\lnot\varphi$ and $\eta(\phi,S,t)>0$. We have $\eta(\varphi,S,t)<0$, and by the induction hypothesis $S\not\models\varphi$. Thus, $S\models\phi$. Similarly, for $\eta(\phi,S,t)<0$ we get $S\nmodels\phi$.

Conjunction: Let $\phi=\varphi_{1}\land\varphi_{2}$ and $\eta(\phi,S,t)>0$. Assume that one or both $\eta(\varphi_{i},S,t)<0$, $i=1,2$, then from (8) we get $\eta(\phi,S,t)=\frac{1}{2}\sum\limits_{i=1,2}[\eta(\varphi_{i},S,t)]_{-}<0$ which contradicts the assumption. It follows that $\eta(\varphi_{i},S,t)>0$, $i=1,2$. By the induction hypothesis $S\models\varphi_{i}$, $i=1,2$, and thus $S\models\phi$. For the case $\eta(\phi,S,t)<0$, assume $\eta(\varphi_{i},S,t)>0$, $i=1,2$. From (7) it follows that $\eta(\phi,S,t)=\sqrt[2]{\prod\limits_{i=1,2}\left({1+\eta({\varphi_{i}},S,t)}\right)}-1>0$ which is a contradiction. Thus, we have either $\eta(\varphi_{1},S,t)<0$ or $\eta(\varphi_{2},S,t)<0$ or both. Again by the induction hypothesis $S\not\models\varphi_{1}$ or $S\not\models\varphi_{2}$, and thus $S\not\models\phi$.

Disjunction: Follows similarly to conjunction case.

Globally: Let $\phi=\mathbf{G}_{[a,b]}\varphi$, and $\eta(\phi,S,t)>0$. Assume that there is $t_{k}^{\prime}\in[t+a,t+b]$ such that $\eta(\varphi,S,t_{k}^{\prime})<0$, then from (8) we get $\eta(\phi,S,t)=\frac{1}{N}\sum\limits_{t_{k}^{\prime}\in[t+a,t+b]}[\eta(\varphi,S,t_{k}^{\prime})]_{-}<0$ which contradicts $\eta(\phi,S,t)>0$. It follows that $\eta(\varphi,S,t_{k}^{\prime})>0$, $\forall t_{k}^{\prime}\in[t+a,t+b]$. By the induction hypothesis $S[t_{k}^{\prime}]\models\varphi$, $\forall t_{k}^{\prime}\in[t+a,t+b]$, and thus $S\models\phi$. For the case $\eta(\phi,S,t)<0$, assume that for all $t_{k}^{\prime}\in[t+a,t+b]$, $\eta(\varphi,S,t_{k}^{\prime})>0$. From (7) we have $\eta(\phi,S,t)=\sqrt[N]{\prod\limits_{t_{k}^{\prime}\in[t+a,t+b]}\left(1+\eta(\varphi,S,t_{k}^{\prime})\right)}-1>0$ which is a contradiction. Thus, we have $\eta(\varphi,S,t_{k}^{\prime})<0$ for some $t_{k}^{\prime}\in[t+a,t+b]$. Again by the induction hypothesis $S[t_{k}^{\prime}]\not\models\varphi$, and thus $S\not\models\phi$.

Eventually: Follows similarly to the globally case. ∎

Proposition 1

Let $S$ be a signal and $\phi$ a STL formula. If $\eta(\phi,S,t)=1$, then $\eta(\varphi,S,t_{k})=1$ for all subformulae $\varphi$ of $\phi$ and appropriate times $t_{k}$ as given by (7), (8). Similarly, if $\eta(\phi,S,t)=0$, then $\eta(\varphi,S,t_{k})=0$ and if $\eta(\phi,S,t)=-1$, then $\eta(\varphi,S,t_{k})=-1$ for all subformulae $\varphi$ of $\phi$ and appropriate times $t_{k}$ in (7), (8).

Proof:

The proof is similar to Theorem 2. ∎

IV-A Logic properties

Let $\bigtriangleup:[-1,1]\times[-1,1]\to[-1,1]$ be a conjunction function defined such that $\bigtriangleup(\eta(\varphi_{1},S),\eta(\varphi_{2},S))=\eta(\varphi_{1}\land\varphi_{2},S)$ for all STL formulae $\varphi_{1},\varphi_{2}$ and signal $S$. Explicitly,

[TABLE]

Proposition 2

The conjunction function satisfies:

[TABLE]

Similarly, we define the disjunction function $\bigtriangledown(\cdot,\cdot)$ which also satisfies the same properties in Proposition 2.

Remark 2

A weaker form of absorption with respect to maximum true and minimum false hold for conjunction $\bigtriangleup(x,-1)<0$ and disjunction $\bigtriangledown(x,1)>0$ for all $x\in(-1,1)$, respectively.

Let $n:[-1,1]\to[-1,1]$ be the negation function defined such that $n(\eta(\varphi,S))=\eta(\lnot\varphi,S)$ for all STL formula $\varphi$ and signal $S$. Explicitly, $n(x)=-x$.

Lastly, we define the implication function $\rhd:[-1,1]\times[-1,1]\to[-1,1]$ as $\rhd(x,y)=\bigtriangledown(-x,y)$.

Theorem 3** (Rules of Inference)**

The following hold:

Law of non-contradiction:* $\bigtriangleup(x,n(x))<0$, $\forall x\neq 0$;* 2. 2.

Law of excluded middle:* $\bigtriangledown(x,n(x))>0$, $\forall x\neq 0$;* 3. 3.

DeMorgan’s law:* $\bigtriangledown(x,y)=n(\bigtriangleup(n(x),n(y)))$, $\forall x,y$;* 4. 4.

Double negation:* $n(n(x))=x$, $\forall x$;* 5. 5.

Modus ponens:* if $\rhd(x,y)>0$ and $x>0$ then $y>0$.*

Proof:

All properties follow directly from the definitions. ∎

Remark 3

Although $([-1,1],\bigtriangleup,\bigtriangledown)$ is not a distributive lattice, i.e., Boolean algebra, it does satisfy the Kleene algebra condition: $\bigtriangleup(x,n(x))\leq\bigtriangledown(y,n(y))$, $\forall x,y\in[-1,1]$.

IV-B Performance Properties

Property 1** (Smoothness and Gradient)**

The AGM robustness $\eta(\phi,S,t)$ is smooth in $S\in[-1,1]^{n}$ almost everywhere except on the satisfaction boundaries $\rho(\varphi,S,t_{k})=0$, where $\varphi$ is a subformula of $\phi$, and appropriate times $t_{k}$ as given in (7) and (8). Moreover, the gradient of $\eta$ with respect to the elements of $S$ that are part of $\phi$’s predicates is non-zero wherever it is smooth.

Proof:

The property follows by structural induction over the formula $\phi$, and the smoothness and non-zero gradient of the conjunction $\bigtriangleup$ and disjunction $\bigtriangledown$ functions on \big{(}(-1,1)\setminus\{0\}\big{)}^{2}, and negation $n$ on $(-1,1)$. The cases for the globally and eventually operators follow similarly. ∎

Property 2** (Arithmetic and Geometric Means)**

By employing arithmetic and geometric means for defining the AGM robustness, we can measure how well a specification $\phi$ is satisfied, taking in to account robustness for all the subformulae $\varphi$ of $\phi$ or at all appropriate times $t_{k}$ and not just the most critical one with maximum/minimum satisfaction. Comparison between traditional and AGM robustness scores demonstrates the advantage of our average-based definition. For instance, consider a signal $S\in[0,1]$ and three subformulae $\varphi_{1},\varphi_{2},\varphi_{3}$ with $\rho(\varphi_{1},S)=\rho(\varphi_{2},S)=\eta(\varphi_{1},S)=\eta(\varphi_{2},S)=1$ and $\rho(\varphi_{3},S)=\eta(\varphi_{3},S)=0.2$. While traditional robustness uses $\max$ function and returns $\rho(\varphi_{1}\vee\varphi_{2},S)=\rho(\varphi_{1}\vee\varphi_{3},S)=1$; AGM definition returns $\eta(\varphi_{1}\vee\varphi_{3},S)=0.6$, which is positive showing that the specification is satisfied, but the robustness is less than $1$ (highest satisfaction), which is attainable only when both subformulae are maximally satisfied, i.e., $\eta(\varphi_{1}\vee\varphi_{2},S)=1$. We now assume $\rho(\varphi_{1},S)=\rho(\varphi_{2},S)=\eta(\varphi_{1},S)=\eta(\varphi_{2},S)=0.2$ and $\rho(\varphi_{3},S)=\eta(\varphi_{3},S)=1$. While traditional robustness uses $\min$ function and returns $\rho(\varphi_{1}\wedge\varphi_{2},S)=\rho(\varphi_{1}\wedge\varphi_{3},S)=0.2$; AGM definition returns $\eta(\varphi_{1}\wedge\varphi_{2},S)=0.2$, which is positive showing the specification is satisfied, but the robustness is less than $\eta(\varphi_{1}\wedge\varphi_{3},S)=0.55$, which shows a stronger satisfaction. Now consider three signals $S_{1},S_{2},S_{3}$ illustrated in Fig. 1. We first examine traditional and AGM robustness score for $\phi_{1}=\mathbf{F}_{[1,4]}(S>0.5)$. Using $\max$ function in the traditional definition, $\rho(\phi_{1},S_{i})=0.5$ for $i=1,2,3$ in Fig. 1 (Left). However, AGM robustness takes a time average over the formula horizon considering all the times the predicate is satisfied; therefore, it returns higher robustness $\eta(\phi_{1},S_{1})=0.5$ for $S_{1}$ and lower robustness $\eta(\phi_{1},S_{2})=0.25$ and $\eta(\phi_{1},S_{3})=0.125$ for $S_{2}$,$S_{3}$, respectively. Basically, AGM robustness for $F_{[a,b]}\varphi$ can be interpreted as “eventually satisfy $\varphi$ with the maximum possible satisfaction as early as possible and for as long as possible”. For signals in Fig. 1 (Right) and $\phi_{2}=\mathbf{G}_{[0,4]}(S>0.5)$, traditional robustness with $\min$ function returns $\rho(\phi_{2},S_{1})=0.5$ for $S_{1}$, while giving same robustness $\rho(\phi_{2},S_{i})=0.1$ for $S_{2},S_{3}$. On the other hand, AGM definition calculates $\eta(\phi_{2},S_{1})=0.5$ for $S_{1}$, and lower robustness scores $\eta(\phi_{2},S_{2})=0.41$ for $S_{2}$ and $\eta(\phi_{2},S_{3})=0.1$ for $S_{3}$. Thus, the AGM definition for $G_{[a,b]}\varphi$ can be interpreted as “always satisfy $\varphi$ with the maximum possible satisfaction for all the time points in $[a,b]$”.