Robust online monitoring of signal temporal logic

Abstract

Signal temporal logic (STL) is a formalism used to rigorously specify requirements of cyberphysical systems (CPS), i.e., systems mixing digital or discrete components in interaction with a continuous environment or analog components. STL is naturally equipped with a quantitative semantics which can be used for various purposes: from assessing the robustness of a specification to guiding searches over the input and parameter space with the goal of falsifying the given property over system behaviors. Algorithms have been proposed and implemented for offline computation of such quantitative semantics, but only few methods exist for an online setting, where one would want to monitor the satisfaction of a formula during simulation. In this paper, we formalize a semantics for robust online monitoring of partial traces, i.e., traces for which there might not be enough data to decide the Boolean satisfaction (and to compute its quantitative counterpart). We propose an efficient algorithm to compute it and demonstrate its usage on two large scale real-world case studies coming from the automotive domain and from CPS education in a Massively Open Online Course setting. We show that savings in computationally expensive simulations far outweigh any overheads incurred by an online approach.

1 Introduction

Design engineers for embedded control software typically validate their designs by inspecting concrete observations of system behavior. For instance, in the model-based development (MBD) paradigm, designers have access to numerical simulation tools to obtain traces from models of systems. An important problem is then to be able to efficiently test whether some logical property $\varphi$ holds for a given simulation trace. It is increasingly common [2, 9, 12, 15, 17] to specify such properties using a real-time temporal logic such as Signal temporal logic (STL) [7] or Metric Temporal Logic (MTL) [10]. An offline monitoring approach involves performing an a posteriori analysis on complete simulation traces (i.e., traces starting at time 0, and lasting till a user-specified time horizon). Theoretical and practical results for offline monitoring [5, 7, 10, 19] focus on the efficiency of monitoring as a function of the length of the trace, and the size of the formula representing the property $\varphi$.

There are a number of situations where offline monitoring is unsuitable. Consider the case where the monitor is to be deployed in an actual system to detect erroneous behavior. As embedded software is typically resource constrained, offline monitoring—which requires storing the entire observed trace—is impractical. Also, when a monitor is used in a simulation-based validation tool, a single simulation may run for several minutes or even hours. If we wish to monitor a safety property over the simulation, a better use of resources is to abort the simulation whenever a violation is detected. Such situations demand an online monitoring algorithm, which has markedly different requirements. In particular, a good online monitoring algorithm must: (1) be able to generate intermediate estimates of property satisfaction based on partial signals, (2) use minimal amount of data storage, and (3) be able to run fast enough in a real-time setting.

Most works on online monitoring algorithms for logics such as Linear Temporal Logic (LTL) or Metric Temporal Logic (MTL) have focussed on the Boolean satisfaction of properties by partial signals [8, 11, 21]. However, recent work has shown that by assigning quantitative semantics to real-time logics such as MTL and STL, problems such as bug-finding, parameter synthesis, and robustness analysis can be solved using powerful off-the-shelf optimization tools [1, 4]. A robust satisfaction value is a function mapping a property $\varphi$ and a trace $\mathbf {x}(t)$ to a real number. A large positive value suggests that $\mathbf {x}(t)$ easily satisfies $\varphi$, a positive value close to zero suggests that $\mathbf {x}(t)$ is close to violating $\varphi$, and a negative value indicates a violation of $\varphi$. While the recursive definitions of quantitative semantics naturally define offline monitoring algorithms to compute robust satisfaction values [5, 7, 10], there is limited work on an online monitoring algorithm to do the same [3].

The main technical and theoretical challenge of online monitoring lies in the definition of a practical semantics for a temporal logic formula over a partial signal, i.e., a signal trace with incomplete data which cannot yet validate or invalidate $\varphi$. Past work [8] has identified three views for the satisfaction of a LTL property $\varphi$ over a partial trace $\tau$: (1) a weak view where the truth value of $\varphi$ over $\tau$ is assigned to true if there is some suffix of $\tau$ that satisfies $\varphi$, (2) a strong view when it is defined to be false when some suffix of $\tau$ does not satisfy $\varphi$ and (3) a neutral view when the truth value is defined using a truncated semantics of LTL restricted to finite paths. In [11], the authors extend the truncated semantics to MTL, and in [3], the authors introduce the notion of a predictor, which works as an oracle to complete the partial trace and provide an estimated satisfaction value. However, such a value cannot be formally trusted in general as long as the data is incomplete.

We now outline our major contributions in this paper. In Sect. 3, we present robust interval semantics for an STL property $\varphi$ on a partial trace $\tau$ that unifies the different semantic views of real-time logics on truncated paths. Informally, the robust interval semantics map a trace $\mathbf {x}(t)$ and an STL property $\varphi$ to an interval $(\ell ,\upsilon )$, with the interpretation that for any suffix u(t), $\ell$ is the greatest lower bound on the quantitative semantics of the trace $\mathbf {x}(t)$, and $\upsilon$ is the corresponding lowest upper bound. There is a natural correspondence between the interval semantics and three-valued semantics: (1) the truth value of $\varphi$ is false according to the weak view iff $\upsilon$ is negative, and true otherwise; (2) the truth value is true according to the strong view iff $\ell$ is positive, and false otherwise; and (3) a neutral semantics, e.g., based on some predictor, can be defined when $\ell<0<\upsilon$, i.e., when there exist both suffixes that can violate or satisfy $\varphi$.

In Sect. 4, we present an efficient online algorithm to compute the robust interval semantics for bounded horizon formulas. Our approach is based on the offline algorithm of [5] extended to work in a fashion similar to the incremental Boolean monitoring of STL implemented in the tool AMT [21]. A key feature of our algorithm is that it imposes minimal runtime overhead with respect to the offline algorithm, while being able to compute robust satisfaction intervals on partial traces. In Sect. 5, we examine the case of unbounded horizon formulas, and present a proof that we can always design a robust online monitor using only a bounded amount of memory.

Finally, we present an implementation and illustrate it with a model of a fuel control system for gasoline engines proposed as industrial benchmark for the verification of Cyber-Physical Systems (CPS) in [14]. We then provide experimental results on two large-scale case studies: (i) industrial-scale Simulink models from the automotive domain in Sect. 6, and (ii) an automatic grading system used in a massive online education initiative on CPS [16]. Since the online algorithm can abort simulation as soon as the truth value of the property is determined, we see a consistent 10–20% savings in simulation time (which is typically several hours) in a majority of experiments, with negligible overhead (<1%). In general, our results indicate that the benefits of our online monitoring algorithm over the offline approach far outweigh any overheads.

2 Background

2.1 Interval arithmetic

We make extensive use of simple interval arithmetic operations which we review next. An interval I is a convex subset of $\mathbb {R}$. A singular interval [a, a] contains exactly one point. Intervals (a, a), [a, a), (a, a], and $\emptyset$ denote empty intervals. We enumerate interval operations below assuming open intervals. Similar operations can be defined for closed, open–closed, and closed–open intervals. In what follows, let $I_j = (a_j,b_j)$.

$$\begin{aligned} -I_1= & {} (-b_1,-a_1) \nonumber \\ c+I_1= & {} (c+a_1, c+b_1) \nonumber \\ I_1 \oplus I_2= & {} (a_1+a_2,b_1+b_2) \nonumber \\ I_1 \cap I_2= & {} \left\{ \begin{array}{ll} \emptyset &{}\text {if}~\min (b_1,b_2) < \max (a_1,a_2) \\ (\max (a_1,a_2), \min (b_1,b_2)) &{} \text {otherwise}. \end{array}\right. \nonumber \\ \min _j(I_j)= & {} (\min \nolimits _j(a_j), \min \nolimits _j(b_j)) \nonumber \\ \max _j(I_j)= & {} (\max \nolimits _j(a_j), \max \nolimits _j(b_j)) \end{aligned}$$

(2.1)

Definition 1

(Signal) A time domain $\mathcal {T}$ is a finite or infinite set of time instants such that $\mathcal {T}\subseteq \mathbb {R}^{\ge 0}$ with $0\in \mathcal {T}$. A signal $\mathbf {x}$ is a function from $\mathcal {T}$ to $\mathcal {X}\subseteq \mathbb {R}^m$ where m is the dimension of the signal. Given a time domain $\mathcal {T}$, a partial signal is any signal defined on a time domain $\mathcal {T}'\subseteq \mathcal {T}$

We remark that we consider the signal-value domain $\mathcal {X}$ to be some compact (bounded and closed) subset of $\mathbb {R}^m$. This is so because we assume that signals are obtained from simulations of physical systems or sensor measurements from a real-world system. In either case, it is reasonable to assume that the signal values come from a bounded set, as physical quantities (e.g., temperature, pressure, velocity) are either inherently bounded, or are limited to the resolution offered by the measurement systems.

Simulation frameworks typically provide signal values at discrete time instants, usually this is a by-product of using a numerical technique to solve the differential equations in the underlying system. These discrete-time solutions are assumed to be sampled versions of the actual signal, which can be reconstructed using some form of interpolation. In this paper, we assume constant interpolation to reconstruct the signal $\mathbf {x}(t)$, i.e., given a sequence of time-value pairs $(t_0,\mathbf {x}_0), \ldots , (t_n,\mathbf {x}_n)$, for all $t \in [t_0,t_n)$, we define $\mathbf {x}(t) = \mathbf {x}_i$ if $t \in [t_i,t_{i+1})$, and $\mathbf {x}(t_n) = \mathbf {x}_n$. Further, let $\mathcal {T}_n \subseteq \mathcal {T}$ represent the finite subset of time instants at which the signal values are given.

2.2 Signal temporal logic

We use signal temporal logic (STL) [7] to analyze time-varying behaviors of signals. We now present its syntax and semantics. A signal predicate $\mu$ is a formula of the form $f(\mathbf {x}) > 0$, where $\mathbf {x}$ is a variable that takes values from $\mathcal {X}$, and f is a function from $\mathcal {X}$ to $\mathbb {R}$. The syntax of an STL formula $\varphi$ is defined as follows:

$$\begin{aligned} \varphi \,{:}{:}{=}\, \mu \mid \lnot \varphi \mid \varphi \wedge \varphi \mid \Box _{I} \varphi \mid \Diamond _{I} \varphi \mid \varphi \mathbf {U}_{I} \varphi \mid \varphi \mathbf {R}_{I} \varphi \end{aligned}$$

(2.2)

Quantitative semantics for timed-temporal logics have been proposed for STL in [7]; we include the definition below.

Definition 2

(Robust satisfaction value) The robust satisfaction value is a function $\rho$ mapping $\varphi$, the signal $\mathbf {x}$, and a time $\tau \in \mathcal {T}$ as follows:

$$\begin{aligned} \rho \left( f(\mathbf {x}) {>} 0, \mathbf {x}, \tau \right)= & {} f(\mathbf {x}(\tau )) \nonumber \\ \rho \left( \lnot \varphi , \mathbf {x}, \tau \right)= & {} -\rho (\varphi ,\mathbf {x},\tau ) \nonumber \\ \rho \left( \varphi _1 \wedge \varphi _2, \mathbf {x}, \tau \right)= & {} \min \left( \rho (\varphi _1,\mathbf {x},\tau ),\rho (\varphi _2,\mathbf {x},\tau )\right) \nonumber \\ \rho \left( \Box _I \varphi , \mathbf {x}, \tau \right)= & {} \displaystyle \inf _{\tau '\in \tau +I} \rho (\varphi ,\mathbf {x},\tau ') \nonumber \\ \rho \left( \Diamond _I \varphi , \mathbf {x}, \tau \right)= & {} \displaystyle \sup _{\tau '\in \tau +I} \rho (\varphi ,\mathbf {x},\tau ') \nonumber \\ \rho \left( \varphi \mathbf {U}_I \psi , \mathbf {x}, \tau \right)= & {} \displaystyle \sup _{\tau _1 \in \tau +I} \min \left( \rho (\psi , \mathbf {x}, \tau _1), \displaystyle \inf _{\tau _2 \in [\tau , \tau _1]} \rho (\varphi , \mathbf {x}, \tau _2) \right) \nonumber \\ \rho \left( \varphi \mathbf {R}_I \psi , \mathbf {x}, \tau \right)= & {} \displaystyle \inf _{\tau _1 \in \tau +I} \max \left( \rho (\psi , \mathbf {x}, \tau _1), \displaystyle \sup _{\tau _2 \in [\tau , \tau _1]} \rho (\varphi , \mathbf {x}, \tau _2) \right) \end{aligned}$$

(2.3)

Here, the translation from quantitative semantics to the usual Boolean satisfaction semantics is that a signal $\mathbf {x}$ satisfies an STL formula $\varphi$ at a time $\tau$ iff the robust satisfaction value $\rho (\varphi ,\mathbf {x},\tau ) \ge 0$. We say a signal $\mathbf {x}$ satisfies $\varphi$ iff $\rho (\varphi , \mathbf {x}) = \rho (\varphi , \mathbf {x}, 0) \ge 0$, i.e., it satisfies $\varphi$ at time 0.

Remark 1

The semantics presented here and in [7, 19] have a technical difference from the ones used in the conventional definition used for Linear Temporal Logic and Metric Temporal Logic (such as in [11]). The difference lies in the definition of $\mathbf {U}$, where for the formula $\varphi \mathbf {U}\psi$, we require $\varphi$ to hold at the time-point at which $\psi$ holds, while previous approaches do require it. (Similarly for the $\mathbf {R}$ operator).

3 Robust interval semantics

In what follows, we assume that we wish to monitor the robust satisfaction value of a signal over a finite time-horizon $T_{H}$. We assume that the signal is obtained by applying piecewise constant interpolation to a sampled signal defined over time-instants $\{t_0,t_1,\ldots ,t_N\}$, such that $t_N = T_{H}$. In an online monitoring context, at any time $t_i$, only the partial signal over time instants $\{t_0, \ldots , t_i\}$ is available, and the rest of the signal becomes available in discrete time increments. We define robust satisfaction semantics of STL formulas over such partial signals using an interval-based semantics. Such a robust satisfaction interval ($\mathtt {RoSI}$) includes all possible robust satisfaction values corresponding to the suffixes of the partial signal. In this section, we formalize the recursive definitions for the robust satisfaction interval of an STL formula with respect to a partial signal, and in the next section we will discuss an efficient algorithm to compute and maintain these intervals.

Definition 3

(Prefix, completions) Let $\{t_0,\ldots ,t_i\}$ be a finite set of time instants such that $t_i \le T_{H}$, and let $\mathbf {x}_{[0,{i}]}$ be a partial signal over the time domain $[t_0,t_i]$. We say that $\mathbf {x}_{[0,{i}]}$ is a prefix of a signal $\mathbf {x}$ if for all $t \le t_i$, $\mathbf {x}(t) = \mathbf {x}_{[0,{i}]}(t)$. The set of completions of a partial signal $\mathbf {x}_{[0,{i}]}$ (denoted by $\mathcal {C}(\mathbf {x}_{[0,{i}]})$) is defined as the set $\{\mathbf {x}\mid \mathbf {x}_{[0,{i}]} \text {is a prefix of}\, \mathbf {x}\}$.

Definition 4

(Robust satisfaction interval ($\mathtt {RoSI}$)) The robust satisfaction interval of an STL formula $\varphi$ on a partial signal $\mathbf {x}_{[0,{i}]}$ at a time $\tau \in [t_0,t_N]$ is an interval I such that:

$$\begin{aligned} \inf (I)= & {} \displaystyle \inf _{\mathbf {x}\in \mathcal {C}(\mathbf {x}_{[0,{i}]})} \rho (\varphi ,\mathbf {x},\tau ) \nonumber \\ \sup (I)= & {} \displaystyle \sup _{\mathbf {x}\in \mathcal {C}(\mathbf {x}_{[0,{i}]})} \rho (\varphi ,\mathbf {x},\tau ) \end{aligned}$$

(3.1)

Definition 5

We now define a recursive function ${[}\rho {]}$ that maps a given formula $\varphi$, a partial signal $\mathbf {x}_{[0,{i}]}$ and a time $\tau \in \mathcal {T}$ to an interval ${[}\rho {]}(\varphi ,\mathbf {x}_{[0,{i}]},\tau )$. We use the notation $f_{\mathsf {inf}}$ and $f_{\mathsf {sup}}$ to respectively denote the infimal and supremal value of the function $f(\mathbf {x})$ over the signal domain $\mathcal {X}$.

$$\begin{aligned} {[}\rho {]}\left( f(\mathbf {x}_{[0,{i}]}){\ge }0, \mathbf {x}_{[0,{i}]}, \tau \right)= & {} \left\{ \begin{array}{ll} [f(\mathbf {x}_{[0,{i}]}(\tau )),f(\mathbf {x}_{[0,{i}]}(\tau ))] &{} \tau \in [t_0,t_i] \\ \,[f_{\mathsf {inf}},f_{\mathsf {sup}}] &{} \text {otherwise.} \end{array}\right. \nonumber \\ {[}\rho {]}\left( \lnot \varphi , \mathbf {x}_{[0,{i}]}, \tau \right)= & {} -{[}\rho {]}(\varphi , \mathbf {x}_{[0,{i}]}, \tau ) \nonumber \\ {[}\rho {]}\left( \varphi _1 \wedge \varphi _2, \mathbf {x}_{[0,{i}]}, \tau \right)= & {} \min ({[}\rho {]}(\varphi _1,\mathbf {x}_{[0,{i}]},\tau ), {[}\rho {]}(\varphi _2,\mathbf {x}_{[0,{i}]},\tau )) \nonumber \\ {[}\rho {]}\left( \Box _I \varphi , \mathbf {x}_{[0,{i}]}, \tau \right)= & {} \displaystyle \inf _{\tau '\in \tau + I} \left( {[}\rho {]}(\varphi ,\mathbf {x}_{[0,{i}]},\tau ')\right) \nonumber \\ {[}\rho {]}\left( \Diamond _I \varphi , \mathbf {x}_{[0,{i}]}, \tau \right)= & {} \displaystyle \sup _{\tau ' \in \tau + I} \left( {[}\rho {]}(\varphi ,\mathbf {x}_{[0,{i}]},\tau ')\right) \nonumber \\ {[}\rho {]}\left( \varphi _1 \mathbf {U}_I \varphi _2, \mathbf {x}_{[0,{i}]}, \tau \right)= & {} \displaystyle \sup _{\tau _1 \in \tau + I} \min \left( \begin{array}{l} {[}\rho {]}(\varphi _2,\mathbf {x}_{[0,{i}]},\tau _1), \\ \displaystyle \inf _{\tau _2 \in [\tau ,\tau _1]} {[}\rho {]}(\varphi _1,\mathbf {x}_{[0,{i}]},\tau _2) \end{array}\right) \nonumber \\ {[}\rho {]}\left( \varphi _1 \mathbf {R}_I \varphi _2, \mathbf {x}_{[0,{i}]}, \tau \right)= & {} \displaystyle \inf _{\tau _1 \in \tau +I} \max \left( \begin{array}{l} {[}\rho {]}(\varphi _2,\mathbf {x}_{[0,{i}]},\tau _1), \\ \displaystyle \sup _{\tau _2 \in [\tau ,\tau _1]} {[}\rho {]}(\varphi _1,\mathbf {x}_{[0,{i}]},\tau _2) \end{array}\right) \end{aligned}$$

(3.2)

The following lemma shows that the interval obtained by applying the recursive definition for ${[}\rho {]}$ is indeed the robust satisfaction interval as defined in Definition 4.

Lemma 1

For any STL formula $\varphi$, the function ${[}\rho {]}(\varphi ,\mathbf {x}_{[0,{i}]},\tau )$ defines the robust satisfaction interval for the formula $\varphi$ over the signal $\mathbf {x}_{[0,{i}]}$ at time $\tau$.

Proof

We prove by induction on the formula structure. The base case is when $\varphi$ is $\mu$. If $\tau \in [t_0,t_i]$ then ${[}\rho {]}(\varphi ,\mathbf {y},\tau )$ = $[f(\mathbf {y}(\tau )),f(\mathbf {y}(\tau ))]$. Let $\mathbf {x}$ be any completion of $\mathbf {y}$. If $\tau \in [t_0,t_i]$ then $\mathbf {x}(\tau ) = \mathbf {y}(\tau )$, and hence, $\inf _{\mathbf {x}\in \mathcal {C}(\mathbf {y})} \rho (\varphi , \mathbf {x}, \tau )$ (resp. $\sup$) is equal to $f(\mathbf {y}(\tau ))$. If $\tau > t_i$, then ${[}\rho {]}(\varphi ,\mathbf {y},\tau ) = [f_{\mathsf {inf}},f_{\mathsf {sup}}]$. By definition of $f_{\mathsf {inf}}$ and $f_{\mathsf {sup}}$, for any completion $\mathbf {x}$, $f(\mathbf {x}(\tau )) \in [f_{\mathsf {inf}},f_{\mathsf {sup}}]$.

We proceed by structural induction on the formula structure. Assume ${[}\rho {]}(\varphi ,\mathbf {y},\tau )$ is a $\mathtt {RoSI}$, i.e., for any completion $\mathbf {x}$ of $\mathbf {y}$, $\rho (\varphi ,\mathbf {x},\tau ) \in {[}\rho {]}(\varphi ,\mathbf {y},\tau )$. As $\rho (\lnot \varphi ,\mathbf {x},\tau )$ = $-\rho (\varphi , \mathbf {x}, \tau )$, it follows that if $\rho (\varphi ,\mathbf {x},\tau ) \in {[}\rho {]}(\varphi ,\mathbf {y},\tau )$, then $-\rho (\varphi ,\mathbf {x},\tau ) \in -{[}\rho {]}(\varphi ,\mathbf {y},\tau )$, by interval arithmetic. For all the remaining operators, we can make a similar argument, and the results follow by the properties of interval arithmetic. $\square$

4 Online algorithm

Donzé et al. [5] present an offline algorithm for monitoring STL formulas over (piecewise) linearly interpolated signals. A naïve implementation of an online algorithm is as follows: at time $t_i$, use a modification of the offline monitoring algorithm to recursively compute the robust satisfaction intervals as defined by Def. 5 to the signal $\mathbf {x}_{[0,{i}]}$. We observe that such a procedure does many repeated computations that can be avoided by maintaining the results of intermediate computations. Furthermore, the naïve procedure requires storing the signal values over the entire time horizon, which makes it memory-intensive. In this section, we present a basic online algorithm for a bounded-horizon fragment of STL.

As in the offline monitoring algorithm in [5], an essential ingredient of the online algorithm is Lemire’s running maximum filter algorithm [18]. The problem this algorithm addresses is the following: given a sequence of values $a_1,\ldots ,a_n$, find the maximum over all windows of size w, i.e., for all j, $\max _{i\in [j,j+w)} a_i$. We briefly review an extension of Lemire’s algorithm over piecewise-constant signals with variable time steps, given as Algorithm 1. The main observation in Lemire’s algorithm is that it is sufficient to maintain a descending monotonic edge (noted $\mathtt {F}$ in Algorithm 1) to compute the sliding maxima, in order to achieve an optimal procedure, measured in terms of the number of comparisons between elements. The first element of $\mathtt {F}$ at time t is the sliding maximum at time t. As F slides forward in time and the window hits a new value $\mathbf {x}_{i+1}$ (Line 6 in Algorithm 1), F is updated by removing every element indexed by the tail of F that are smaller than $\mathbf {x}_{i+1}$ (Line 7–8), then $i+1$ becomes the tail. It can be shown that with this mechanism, the total number of comparisons between elements is linear in the total number of values. Algorithm 1 extends [18] in that it deals with timed values (or piecewise constant signals) instead of a simple discrete array and is slightly simpler than the one in [5] which considers piecewise linear signals, i.e., linear interpolation between values.

4.1 Stipulation on time-step

As in the offline algorithm, we stipulate that the signal being monitored has finite variability. We formalize this in terms of a minimum time-step in the signal. Given a signal $\mathbf {x}(t)$ as a sequence of time-value pairs $(t_0,\mathbf {x}_0),\ldots ,(t_n,\mathbf {x}_n)$, we require n to be a finite integer, and we require that there exist a known $\varDelta \in \mathbb {R}^{> 0}$, such for any $i \ge 0$, $t_{i+1} - t_i > \varDelta$.

We observe that the knowledge of such a “minimum time-step” $\varDelta$ known a priori is a reasonable assumption for most real-time monitoring scenarios. This is so because, it is physically impossible for a monitoring routine to samples the actual dense-time signal at an infinite resolution, i.e., some time must pass between consecutive samples in the signal.

We now present the algorithm for the fragment of STL where each temporal operator is bounded by a time-interval I such that $\sup (I)$ is finite. The procedure for online monitoring is an algorithm that maintains in memory the syntax tree of the formula $\varphi$ to be monitored, augmented with some book-keeping information. First, we formalize some notation. For a given formula $\varphi$, let $\mathcal {T}_{\varphi }$ represent the syntax tree of $\varphi$, and let $\mathsf {root}(\mathcal {T}_{\varphi })$ denote the root of the tree. Each node in the syntax tree (other than a leaf node) corresponds to an STL operator $\lnot , \vee , \wedge , \Box _I$ or $\Diamond _I$. We omit the case of $\mathbf {U}_I$ here for clarity of the presentation - simply note that the rewriting approach of [5] can also be adapted and was implemented in our tool. We will use $\mathbf {H}_I$ to denote any temporal operator bounded by interval I. For a given node $v$, let $\mathsf {op}(v)$ denote the operator for that node. For any node $v$ in $\mathcal {T}_{\varphi }$ (except the root node), let $\mathsf {parent}(v)$ denote the unique parent of $v$.

Algorithm 2 does the online $\mathtt {RoSI}$ computation. Like the offline algorithm, it is a dynamic programming algorithm operating on the syntax tree of the given STL formula, i.e., computation of the $\mathtt {RoSI}$ of a formula combines the $\mathtt {RoSI}$s for its constituent sub-formulas in a bottom-up fashion. As computing the $\mathtt {RoSI}$ at a node $v$ requires the $\mathtt {RoSI}$s at the child-nodes, this computation has to be delayed till the $\mathtt {RoSI}$s at the children of $v$ in a certain time-interval are available. We call this time-interval the time horizon of $v$ (denoted $\mathsf {hor}(v)$), and define it recursively in Eq. (4.1).

$$\begin{aligned} \mathsf {hor}(v) =\left\{ \begin{array}{ll} [0] &{}\text {if}~v= \mathsf {root}(\mathcal {T}_{\varphi })\\ I \oplus \mathsf {hor}(\mathsf {parent}(v)) &{} \text {if}~v\ne \mathsf {root}(\mathcal {T}_{\varphi }) \text{ and } \mathsf {op}(\mathsf {parent}(v)) = \mathbf {H}_I \\ \mathsf {hor}(\mathsf {parent}(v)) &{}\text {otherwise}. \end{array} \right. \end{aligned}$$

(4.1)

We illustrate the working of the algorithm using a small example then give a brief sketch of the various steps in the algorithm.

Example 1

Consider formula (4.2). We show $\mathcal {T}_{\varphi }$ and $\mathsf {hor}(v)$ for each node $v$ in $\mathcal {T}_{\varphi }$ in Fig. 1. In rest of the paper, we use $\varphi$ as a running example.¹

$$\begin{aligned} \varphi \triangleq \Box _{[0,a]}\left( \lnot (y>0)\vee \Diamond _{[b,c]}(x>0)\right) \end{aligned}$$

(4.2)

The algorithm augments each node $v$ of $\mathcal {T}_{\varphi }$ with a double-ended queue, that we denote $\mathsf {worklist}[v]$. Let $\psi$ be the subformula denoted by the tree rooted at $v$. For the partial signal $\mathbf {x}_{[0,{i}]}$, the algorithm maintains in $\mathsf {worklist}[v]$, the $\mathtt {RoSI}$ ${[}\rho {]}(\psi , \mathbf {x}_{[0,{i}]}, t)$ for each $t \in \mathsf {hor}(v) \cap [t_0,t_i]$. We denote by $\mathsf {worklist}[v](t)$ the entry corresponding to time t in $\mathsf {worklist}[v]$. When a new data-point $\mathbf {x}_{i+1}$ corresponding to the time $t_{i+1}$ is available, the monitoring procedure updates each ${[}\rho {]}(\psi ,\mathbf {x}_{[0,{i}]},t)$ in $\mathsf {worklist}[v]$ to ${[}\rho {]}(\psi ,\mathbf {x}_{[0,{i+1}]},t)$(Fig. 2).

In Fig. 3, we give an example of a run of the algorithm on the plots shown in Fig. 2. We assume that the algorithm starts in a state where it has processed the partial signal $\mathbf {x}_{[0,{2}]}$, and show the effect of receiving data at time-points $t_3$, $t_4$ and $t_5$. The figure shows the states of the worklists at each node of $\mathcal {T}_{\varphi }$ at these times when monitoring the STL formula $\varphi$ presented in Eq. (4.2). Each row in the table adjacent to a node shows the state of the worklist after the algorithm processes the value at the time indicated in the first column.

The first row of the table shows the snapshot of the worklists at time $t_2$. Observe that in the worklists for the subformula $y>0$, $\lnot y>0$, because $a<b$, the data required to compute the $\mathtt {RoSI}$ at $t_0$, $t_1$ and the time a, is available, and hence each of the $\mathtt {RoSI}$s is singular. On the other hand, for the subformula $x>0$, the time horizon is $[b,a+c]$, and no signal value is available at any time in this interval. Thus, at time $t_2$, all elements of $\mathsf {worklist}[v_{x>0}]$ are $({\mathbf {x}_{\mathsf {inf}}},{\mathbf {x}_{\mathsf {sup}}})$ corresponding to the greatest lower bound and lowest upper bound on x.

Fig. 1

Syntax tree $\mathcal {T}_{\varphi }$ for $\varphi$ [given in (4.2)] with each node $v$ annotated with $\mathsf {hor}(v)$

To compute the values of $\Diamond _{[b,c]}(x>0)$ at any time t, we take the supremum over values from times $t+b$ to $t+c$. As the time horizon for the node corresponding to $\Diamond _{[b,c]} (x>0)$ is [0, a], t ranges over [0, a]. In other words, we wish to perform the sliding maximum over the interval $[0+b, a+c]$, with a window of length $c-b$. We can use the algorithm for computing the sliding window maximum as discussed earlier in this section. One caveat is that we need to store separate monotonic edges for the upper and lower bounds of the $\mathtt {RoSI}$s. The algorithm then proceeds upward on the syntax tree, only updating the worklist of a node only when there is an update to the worklists of its children.

The second row in each table is the effect of obtaining a new time point (at time $t_3$) for both signals. Note that this does not affect $\mathsf {worklist}[v_{y>0}]$ or $\mathsf {worklist}[v_{\lnot y>0}]$, as all $\mathtt {RoSI}$s are already singular, but does update the $\mathtt {RoSI}$ values for the node $v_{x>0}$. The algorithm then invokes Algorithm 1 on $\mathsf {worklist}[v_{x>0}]$ to update $\mathsf {worklist}[v_{\Diamond _{[b,c]}(x>0)}]$. Note that in the invocation on the second row (corresponding to time $t_3$), there is an additional value in the worklist, at time $t_3$. This leads Algorithm 1 to produce a new value of $\mathsf {SlidingMax}\left( \mathsf {worklist}[v_{\mathbf {x}>0}],[b,c]\right) (t_3-b)$, which is then inserted in $\mathsf {worklist}[v_{\Diamond _{[b,c]} x>0}]$. This leads to additional points appearing in worklists at the ancestors of this node.

Finally, we remark that the run of this algorithm shows that at time $t_4$, the $\mathtt {RoSI}$ for the formula $\varphi$ is $[-2,-2]$, which yields a negative upper bound, showing that the formula is not satisfied irrespective of the suffixes of x and y. In other words, the satisfaction of $\varphi$ is known before we have all the data required by $\mathsf {hor}(\varphi )$.

Fig. 2

These plots show the signals x(t) and y(t). Each signal begins at time $t_0 = 0$, and we consider three partial signals: $\mathbf {x}_{[0,{3}]}$ (black  $+$ blue), and $\mathbf {x}_{[0,{4}]}$ ($\mathbf {x}_{[0,{3}]}\,+$  green), and $\mathbf {x}_{[0,{5}]}$ ($\mathbf {x}_{[0,{4}]}\,+\,$ red). (Color figure online)

Fig. 3

We show a snapshot of the $\mathsf {worklist}[v]$ maintained by the algorithm for four different (incremental) partial traces of the signals x(t) and y(t). Each row indicates the state of $\mathsf {worklist}[v]$ at the time indicated in the first column. An entry marked -- indicates that the corresponding element did not exist in $\mathsf {worklist}[v]$ at that time. Each colored entry indicates that the entry was affected by availability of a signal fragment of the corresponding color. (Color figure online)

Algorithm 2 is essentially a procedure that recursively visits each node in the syntax tree $\mathcal {T}_{\varphi }$ of the STL formula $\varphi$ that we wish to monitor. Line 4 corresponds to the base case of the recursion, i.e. when the algorithm visits a leaf of $\mathcal {T}_{\varphi }$ or an atomic predicates of the form $f(\mathbf {x}) > 0$. Here, the algorithm inserts the pair $(t_{i+1},\mathbf {x}_{i+1})$ in $\mathsf {worklist}[v_{f(\mathbf {x})>0}]$ if $t_{i+1}$ lies inside $\mathsf {hor}(v_{f(\mathbf {x})>0})$. In other words, it only tracks a value if it is useful for the computing the robust satisfaction interval of some ancestor node.

For a node corresponding to a Boolean operation, the algorithm first updates the worklists at the children, and then uses them to update the worklist at the node. If the current node represents $\lnot \varphi$ (Line 5), the algorithm flips the sign of each entry in $\mathsf {worklist}[v_\varphi ]$; this operation is denoted as $-\mathsf {worklist}[v_\varphi ]$. Consider the case where the current node $v_{\psi }$ is a conjunction $\varphi _1 \wedge \varphi _2$. The sequence of upper bounds and the sequence of lower bounds of the entries in $\mathsf {worklist}[v_{\varphi _1}]$ and $\mathsf {worklist}[v_{\varphi _1}]$ can be each thought of as a piecewise-constant signal (likewise for $\mathsf {worklist}[v_{\varphi _2}]$). In Line 11, the algorithm computes a pointwise-minimum over piecewise-constant signals representing the upper and lower bounds of the $\mathtt {RoSI}$s of its arguments. Note that for $i=1,2$, if $\mathsf {worklist}[v_{\varphi _i}]$ has $N_i$ entries, then the pointwise-$\min$ would have to be performed at most $N_1 + N_2$ distinct time-points. Thus, $\mathsf {worklist}[v_{\varphi _1 \wedge \varphi _2}]$ has at most $N_1 + N_2$ entries. A similar phenomenon can be seen in Fig. 3, where computing a $\max$ over the worklists of $v_{\Diamond _{[b,c](x>0)}}$ and $v_{\lnot (y>0)}$ leads to an increase in the number of entries in the worklist of the disjunction.

For nodes corresponding to temporal operators, e.g., $\Diamond _I \varphi$ or $\Box _I \varphi$, the algorithm first updates $\mathsf {worklist}[v_\varphi ]$. It then applies Algorithm 1 to compute the sliding maximum over $\mathsf {worklist}[v_\varphi ]$ for $\Diamond _I$. For $\Box _I$, the expression $-\mathsf {SlidingMax}(-\mathsf {worklist}[v_\varphi ], I)$ effectively computes the sliding minimum by reusing the $\mathsf {SlidingMax}$ algorithm. Note that if $\mathsf {worklist}[v_\varphi ]$ contains N entries, so does $\mathsf {worklist}[v_{\Diamond _I\varphi }]$ or $\mathsf {worklist}[v_{\Box _I\varphi }]$. We note that the minimum time-step stipulation enforces that all the worklists have a finite number of elements.

A further optimization can be implemented on top of this basic scheme. For a node $v$ corresponding to the subformula $\mathbf {H}_I \varphi$, the first few entries of $\mathsf {worklist}[v]$ (say up to time u) could become singular intervals once the required $\mathtt {RoSI}$s for $\mathsf {worklist}[v_\varphi ]$ are available. The optimization is to only compute $\mathsf {SlidingMax}$ over $\mathsf {worklist}[v_\varphi ]$ starting from $u + \inf (I)$. We omit the pseudo-code for brevity. Finally, we remark that the robust satisfaction interval shrinks (or stays the same) with every new time-point in the signal that becomes available, and never grows.

5 Nominal semantics and monitoring untimed formulas

In the previous section, we presented a monitoring algorithm for STL formulas with a bounded time-horizon. In this section, we consider STL formulas that may have temporal operators with an unbounded time-horizon. We first make the observation that the robust interval semantics for a large class of unbounded-horizon STL formulas such as $\Box \Diamond (f(\mathbf {x}) > 0)$, or $\Box (\varphi \implies \Diamond \psi )$ is trivially $[f_{\mathsf {inf}},f_{\mathsf {sup}}]$.

Clearly, considering robust interval semantics for unbounded horizon STL formulas is thus trivial and not useful, as it does not give any information. In this section, we define nominal robust semantics for the purpose of online monitoring.

5.1 Nominal semantics

The nominal semantics of an STL formula can be described in terms of the recursive function $\rho _{\mathrm{nom}}$ that maps a given formula $\varphi$, a partial signal $\mathbf {x}_{[0,{i}]}$ and a time $\tau \in \mathcal {T}$ to a value $\rho _{\mathrm{nom}}(\varphi ,\mathbf {x}_{[0,{i}]},\tau )$.

(5.1)

Observe that the nominal robust satisfaction value closely matches the usual definition for the robust satisfaction value, except that for the unbounded temporal operators, the robustness computation is restricted to the signal values available at time $t_i$.

Note that the algorithm to compute robust interval satisfaction could be used to compute the nominal robust satisfaction, but a direct application of Algorithm 2 requires every node in the sub-tree rooted at the untimed operator to have a time horizon that is equal to the time horizon for the trace. In other words, for all such nodes, the algorithm would have to keep track of every value over arbitrarily long intervals. In what follows, we show that we can monitor arbitrary STL formulas using amount of memory that is trace-length independent, such that the bound is exponential in the size of the formula. We first establish this result for a fragment of STL (denoted STL_u) that does not contain any bounded time-horizon temporal operators, and then indicate how it can be generalized to entire STL.

In what follows, we assume that the domain of signals is a compact set, and replace $\inf$ and $\sup$ by $\min$ and $\max$ respectively. The syntax of a formula $\varphi$ in STL_u is as defined in (5.2). Here, $\mu$ indicates a predicate over signals, same as the one defined for STL in (2.2). Note that in STL_u we assume that all negations are pushed to the $\mu$ atoms using standard rewrite rules for STL.

$$\begin{aligned} \varphi \,{:}{:}{=}\,\mu \mid \varphi \wedge \varphi \mid \varphi \vee \varphi \mid \Box \varphi \mid \Diamond \varphi \mid \varphi \mathbf {U}\varphi \varphi \mathbf {R}\varphi \end{aligned}$$

(5.2)

Proposition 1

For $t_i \in [t_0,t_{n-1}]$, we can always rewrite the nominal robustness of a STL_u formula as an expression of the following form:

$$\begin{aligned} \rho _{\mathrm{nom}}(\phi , \mathbf {x}_{[0,{n}]}, t_i) = \max \left( \begin{array}{l} \alpha (n), \\ \min \left( {\beta _1}(n), \rho _{\mathrm{nom}}(\zeta _1, \mathbf {x}_{[0,{n-1}]}, t_i)\right) \\ \vdots \\ \min \left( {\beta _k}(n), \rho _{\mathrm{nom}}(\zeta _k, \mathbf {x}_{[0,{n-1}]}, t_i)\right) \end{array}\right) \end{aligned}$$

(5.3)

We prove this proposition using structural induction on STL_u formulas. We use the following expression as an abbrevication for the expression in Eq. (5.3):

$$\begin{aligned} E\left( t_i, \alpha (n), (\beta _1(n),\zeta _1), \ldots , (\beta _k(n), \zeta _k) \right) . \end{aligned}$$

Note that the values $\alpha (n)$ or $\beta _\ell (n)$, $\ell \in [1,k]$, could be $-\infty$ or $+\infty$. Further, if a $\beta _\ell (n)$ value is $-\infty$, then this term can be dropped from the expression, and if an $\alpha (n)$ value is $+\infty$, then the whole expression evaluates to $+\infty$ (possibly indicating that the formula being monitored is a tautology).

5.2 Intuition for computing memory bounds

In the above expression, $\alpha (n)$ and ${\beta _j}(n)$ are meant to represent concrete numeric values evaluate that are computed from the formula to be monitored using trace-values only for time $t_n$. The $\zeta _j$ formulas are some STL_u formulas related to the original formula. This relation will become clearer from the proofs of the lemmata to follow. Each of the expression $\rho _{\mathrm{nom}}(\zeta _\ell , \mathbf {x}_{[0,{n-1}]}, t_i)$ represents a variable that stores the nominal robustness of the formula $\zeta _\ell$ over the partial signal $\mathbf {x}_{[0,{n-1}]}$. In other words, each such formula represents a summary of the computation till time $t_{n-1}$. Thus, for any given formula, the number of the $\zeta$ terms in the expression to compute the nominal robustness of that formula determines how many variables required. Thus, if the number of $\zeta$ terms is finite, i.e., dependent only on the length of the formula, and independent of the trace-length, then we can monitor the robust nominal robustness over unbounded horizon temporal formulas with finite memory.

5.3 Intuition for the inductive hypothesis

The main intuition for the inductive hypothesis is that for any STL_u formula, the expression for the nominal robustness can always be rewritten as a “sum of products” form, i.e., as a $\max$ of (1) a specific numeric value obtained only from the signal value at time $t_n$, and (2) expressions representing the $\min$ of a summary variable representing computation over the signal values from time $t_0$ to $t_{n-1}$ with a specific numeric value computed only using the data at time $t_n$.

We now prove the validity of the proposition by structural induction over the formula structure, i.e., assuming that the hypothesis holds for subformulas, we prove that the hypothesis holds for the formula constructed using the subformulas. We start with the base case where the STL_u formula is an atomic proposition, and show that the induction hypothesis is valid for this case.

Lemma 2

(Base Case) The nominal robustness for a formula $\mu$, where $\mu \equiv (f(\mathbf {x})>0)$ at time $t_i \in [t_0,t_{n-1}]$ over the partial signal $\mathbf {x}_{[0,{n}]}$ can be written as an expression of the form in Eq. (5.3).

Proof

As the nominal robustness for $\mu$ at time $t_i \in [t_0,t_{n-1}]$ is independent of $\mathbf {x}(t_n)$, we can see that $\rho _{\mathrm{nom}}(\mu , \mathbf {x}_{[0,{n}]}, t_i)$ is equivalent to $\rho _{\mathrm{nom}}(\mu , \mathbf {x}_{[0,{n-1}]}, t_i)$, which can be written as $\max (-\infty , \min (\infty , \rho _{\mathrm{nom}}(\mu , \mathbf {x}_{[0,{n-1}]}, t_i)))$, i.e. $E\left( t_i, -\infty ,(+\infty ,\mu )\right)$. $\square$

We now establish Proposition 1 inductively for other kinds of STL_u formulas.

Lemma 3

The nominal robustness of $\varphi _1 \wedge \varphi _2$ at time $t_i \in [t_0,t_{n-1}]$ over the partial signal $\mathbf {x}_{[0,{n}]}$ can be written as an expression of the form (5.3).

Proof

By definition of nominal robustness,

$$\begin{aligned} \rho _{\mathrm{nom}}(\varphi _1 \wedge \varphi _2, \mathbf {x}_{[0,{n}]}, t_i) = \min (\rho _{\mathrm{nom}}(\varphi _1, \mathbf {x}_{[0,{n}]}, t_i), \rho _{\mathrm{nom}}(\varphi _2, \mathbf {x}_{[0,{n}]}, t_i)). \end{aligned}$$

(5.4)

Using the induction hypothesis, we can replace each argument of the $\min$ as follows:

$$\begin{aligned} \min \left( \begin{array}{l} \max \left( \begin{array}{l} \alpha ^1(n), \\ \min \left( {\beta ^1_1}(n), \rho _{\mathrm{nom}}\left( \zeta ^1_1, \mathbf {x}_{[0,{n-1}]}, t_i\right) \right) , \\ \ldots \\ \min \left( {\beta ^1_{k_1}}(n), \rho _{\mathrm{nom}}\left( \zeta ^1_{k_1}, \mathbf {x}_{[0,{n-1}]}, t_i\right) \right) \end{array}\right) , \\ \max \left( \begin{array}{l} \alpha ^2(n), \\ \min \left( {\beta ^2_1}(n), \rho _{\mathrm{nom}}\left( \zeta ^2_1, \mathbf {x}_{[0,{n-1}]}, t_i\right) \right) , \\ \ldots , \\ \min \left( {\beta ^2_{k_2}}(n), \rho _{\mathrm{nom}}\left( \zeta ^2_{k_2}, \mathbf {x}_{[0,{n-1}]}, t_i\right) \right) \end{array}\right) \end{array}\right) \end{aligned}$$

(5.5)

Using the rule $\min (\max (a,b),\max (c,d))$ = $\max (\min (a,c),\min (a,d),\min (b,c),\min (b,d))$, we can rewrite the above formula as follows:

$$\begin{aligned} \max \left( \begin{array}{l} \min \left( \alpha ^1(n),\alpha ^2(n)\right) , \\ \displaystyle \min _{\ell \in [1,k_1]} \left( \alpha ^1(n), {\beta ^2_\ell }(n), \rho _{\mathrm{nom}}\left( \zeta ^2_\ell , \mathbf {x}_{[0,{n-1}]}, t_i\right) \right) , \\ \displaystyle \min _{m \in [1,k_2]} \left( \alpha ^2(n), {\beta ^1_m}(n), \rho _{\mathrm{nom}}\left( \zeta ^1_m, \mathbf {x}_{[0,{n-1}]}, t_i\right) \right) , \\ \displaystyle \min _{\ell \in [1,k_1]}\displaystyle \min _{m \in [1, k_2]} \left( \min \left( \beta ^1_\ell , \beta ^2_m, \rho _{\mathrm{nom}}\left( \zeta ^1_\ell \wedge \zeta ^2_m, \mathbf {x}_{[0,{n-1}]}, t_i\right) \right) \right) \end{array}\right) \end{aligned}$$

(5.6)

Observe that the above formula is of the following form that preserves the induction hypothesis:

$$\begin{aligned} {E\left( t_i, \begin{array}{lll} \min \left( \alpha ^1(n),\alpha ^2(n)\right) , &{} &{} \\ \left( \min \left( \alpha ^1(n), \beta ^2_1(n)\right) ,\ \zeta ^2_1\right) , &{} \ldots , &{} \left( \min \left( \alpha ^1(n), \beta ^2_{k_2}(n)\right) ,\ \zeta ^2_{k_2}\right) \\ \left( \min \left( \alpha ^2(n), \beta ^1_1(n)\right) ,\ \zeta ^2_1\right) , &{} \ldots , &{} \left( \min \left( \alpha ^2(n), \beta ^1_{k_1}(n)\right) ,\ \zeta ^2_{k_1}\right) , \\ \left( \min \left( \beta ^1_1(n),\beta ^2_1(n)\right) ,\ \zeta ^1_1 \wedge \zeta ^2_1)\right) &{} \ldots &{} \left( \min \left( \beta ^1_1(n),\beta ^2_{k_2}(n)\right) ,\ \zeta ^1_1 \wedge \zeta ^2_{k_2}\right) , \\ \vdots &{} \ddots &{} \vdots \\ \left( \min \left( \beta ^1_{k_1}(n),\beta ^2_{1}(n)\right) ,\ \zeta ^1_{k_1} \wedge \zeta ^2_{1}\right) , &{} \ldots , &{} \left( \min \left( \beta ^1_{k_1}(n),\beta ^2_{k_2}(n)\right) ,\ \zeta ^1_{k_1} \wedge \zeta ^2_{k_2}\right) \\ \end{array} \right) } \end{aligned}$$

(5.7)

We observe that if the expressions for $\varphi _1$ and $\varphi _2$ respectively have $k_1 + 1$ and $k_2 + 1$ terms, then the expression for $\varphi _1 \wedge \varphi _2$ has $(k_1 + 1)(k_2 + 1)$ terms. $\square$

Lemma 4

The nominal robustness of $\varphi _1 \vee \varphi _2$ at time $t_i \in [t_0,t_{n-1}]$ over the partial signal $\mathbf {x}_{[0,{n}]}$ can be written as an expression of the form (5.3).

Proof

By definition of nominal robustness,

$$\begin{aligned} \rho _{\mathrm{nom}}(\varphi _1 \vee \varphi _2, \mathbf {x}_{[0,{n}]}, t_i) = \max (\rho _{\mathrm{nom}}(\varphi _1, \mathbf {x}_{[0,{n}]}, t_i), \rho _{\mathrm{nom}}(\varphi _2, \mathbf {x}_{[0,{n}]}, t_i)). \end{aligned}$$

(5.8)

Using the induction hypothesis, we can replace each argument of the $\min$ as follows:

$$\begin{aligned} \max \left( \begin{array}{l} \max \left( \begin{array}{l} \alpha ^1(n), \\ \min \left( {\beta ^1_1}(n), \rho _{\mathrm{nom}}\left( \zeta ^1_1, \mathbf {x}_{[0,{n-1}]}, t_i\right) \right) , \\ \ldots \\ \min \left( {\beta ^1_{k_1}}(n), \rho _{\mathrm{nom}}\left( \zeta ^1_{k_1}, \mathbf {x}_{[0,{n-1}]}, t_i\right) \right) \end{array}\right) , \\ \max \left( \begin{array}{l} \alpha ^2(n), \\ \min \left( {\beta ^2_1}(n), \rho _{\mathrm{nom}}\left( \zeta ^2_1, \mathbf {x}_{[0,{n-1}]}, t_i\right) \right) , \\ \ldots , \\ \min \left( {\beta ^2_{k_2}}(n), \rho _{\mathrm{nom}}\left( \zeta ^2_{k_2}, \mathbf {x}_{[0,{n-1}]}, t_i\right) \right) \end{array}\right) \end{array}\right) \end{aligned}$$

(5.9)

Observe that the above formula is of the following form that preserves the induction hypothesis:

$$\begin{aligned} E\left( t_i, \begin{array}{l} \max \left( \alpha ^1(n), \alpha ^2(n)\right) , \\ \left( \beta ^1_1(n),\ \zeta _1^1\right) , \ldots , \left( \beta ^1_{k_1}(n),\ \zeta _{k_1}^1\right) , \\ \left( \beta ^2_1(n),\ \zeta _1^2\right) , \ldots , \left( \beta ^2_{k_2}(n),\ \zeta _{k_2}^2\right) \end{array} \right) \end{aligned}$$

(5.10)

Observe that if $\varphi _1$ and $\varphi _2$ have $k_1$ and $k_2$ summary variables respectively, $\varphi _1 \vee \varphi _2$ requires $k_1 + k_2$ summary variables. $\square$

Lemma 5

The nominal robustness of $\Diamond \varphi$ at time $t_i \in [t_0,t_{n-1}]$ over the partial signal $\mathbf {x}_{[0,{n}]}$ can be written as an expression of the form (5.3).

Proof

By definition of nominal robustness of $\Diamond \varphi$,

$$\begin{aligned} \begin{array}{ll} \rho _{\mathrm{nom}}(\Diamond \varphi , \mathbf {x}_{[0,{n}]}, t_i) &{} = \displaystyle \max _{t_j \in [t_i,t_n]} \rho _{\mathrm{nom}}(\varphi , \mathbf {x}_{[0,{n}]}, t_j) \\ &{} = \max \left( \varphi (n), \displaystyle \max _{t_j \in [t_i, t_{n-1}]} \rho _{\mathrm{nom}}(\varphi , \mathbf {x}_{[0,{n-1}]}, t_j) \right) \end{array} \end{aligned}$$

(5.11)

The above is obtained by splitting the outer $\max$ into a term over time points between $t_i$ and $t_{n-1}$ and a second term containing the evaluation of the nominal robustness of the formula $\varphi$ at time $t_n$. Note that for any formula $\varphi$, the nominal robustness at time $t_n$ is a concrete value that can be computed using the recursive semantics. We call this value $\varphi (n)$. We now use the inductive hypothesis (Eq. (5.3)) for $\rho _{\mathrm{nom}}(\varphi ,\mathbf {x}_{[0,{n}]},t_j)$:

$$\begin{aligned} \max \left( \varphi (n), \displaystyle \max _{t_j\in [t_i,t_{n-1}]}\left( \alpha (n), \displaystyle \max _{\ell \in [1,k]} \min \left( \beta _\ell (n), \rho _{\mathrm{nom}}(\zeta _\ell , \mathbf {x}_{[0,{n-1}]}, t_j) \right) \right) \right) \end{aligned}$$

(5.12)

Grouping the $\alpha (n)$ term,

$$\begin{aligned} = \max \left( \alpha (n), \varphi (n), \displaystyle \max _{t_j \in [t_i,t_n]} \displaystyle \max _{\ell \in [1,k]} \left( \min \left( \beta _1(n), \rho _{\mathrm{nom}}(\zeta _1, \mathbf {x}_{[0,{n-1}]}, t_j) \right) \right) \right) \end{aligned}$$

(5.13)

Distributing the inner $\max$ over individual time points $t_j \in [t_i,t_n]$:

$$\begin{aligned} = \max \left( \alpha (n), \varphi (n), \max \left( \begin{array}{l} \displaystyle \max _{\ell \in [1,k]} \min \left( \beta _\ell (n), \rho _{\mathrm{nom}}(\zeta _\ell , \mathbf {x}_{[0,{n-1}]}, t_i) \right) , \\ \displaystyle \max _{\ell \in [1,k]} \min \left( \beta _\ell (n), \rho _{\mathrm{nom}}(\zeta _\ell , \mathbf {x}_{[0,{n-1}]}, t_{i+1}) \right) , \\ \ldots , \\ \displaystyle \max _{\ell \in [1,k]} \min \left( \beta _\ell (n), \rho _{\mathrm{nom}}(\zeta _\ell , \mathbf {x}_{[0,{n-1}]}, t_{n-1}) \right) \end{array}\right) \right) . \end{aligned}$$

(5.14)

Observe that for each $\ell \in [1,k]$, we can use the following rule to group expressions containing $\beta _\ell (n)$ terms: $\max (\min (a,b),\min (a,c))$ = $\min (a,\max (b,c))$. Furthermore, based on the definition of $\Diamond$, we can have that $\max _{t_j\in [t_i,t_{n-1}]} \rho _{\mathrm{nom}}(\zeta _\ell ,\mathbf {x}_{[0,{n-1}]},t_j)$ is equivalent to $\rho _{\mathrm{nom}}(\Diamond \zeta _\ell ,\mathbf {x}_{[0,{n-1}]},t_i)$.

$$\begin{aligned} = \max \left( \begin{array}{l} \max (\alpha (n),\varphi (n)) \\ \min (\beta _1(n), \rho _{\mathrm{nom}}(\Diamond \zeta _1, \mathbf {x}_{[0,{n-1}]}, t_i)), \\ \ldots , \\ \min (\beta _k(n), \rho _{\mathrm{nom}}(\Diamond \zeta _k, \mathbf {x}_{[0,{n-1}]}, t_i)) \end{array} \right) \end{aligned}$$

(5.15)

The above expression is of the following form, which matches the inductive hypothesis specified in Eq. (5.3): $E\left( t_i, \max (\varphi (n),\alpha (n)), \left( \beta _1(n),\ \Diamond \zeta _1\right) , \ldots , \left( \beta _k,\ \Diamond \zeta _k\right) \right)$. Furthermore, observe that if $\varphi$ requires k summary variables, $\Diamond \varphi$ also requires k summary variables. $\square$

Lemma 6

The nominal robustness of $\Box \varphi$ at time $t_i \in [t_0,t_{n-1}]$ for the partial signal $\mathbf {x}_{[0,{n}]}$ can be written as an expression of the form (5.3).

Proof

By definition of nominal robustness of $\Box \varphi$,

$$\begin{aligned} \begin{array}{ll} \rho _{\mathrm{nom}}(\Box \varphi , \mathbf {x}_{[0,{n}]}, t_i) &{} = \displaystyle \min _{t_j \in [t_i,t_n]} \rho _{\mathrm{nom}}(\varphi , \mathbf {x}_{[0,{n}]}, t_j) \\ &{} = \min \left( \varphi (n), \displaystyle \min _{t_j \in [t_i,t_{n-1}]} \rho _{\mathrm{nom}}(\varphi , \mathbf {x}_{[0,{n}]}, t_j) \right) \end{array} \end{aligned}$$

(5.16)

As before, we use the inductive hypothesis for $\rho _{\mathrm{nom}}(\varphi ,\mathbf {x}_{[0,{n}]},t_j)$:

$$\begin{aligned} = \min \left( \varphi (n), \displaystyle \min _{t_j \in [t_i,t_{n-1}]} \max \left( \alpha (n), \displaystyle \max _{\ell \in [1,k]} \min \left( \beta _\ell (n), \rho _{\mathrm{nom}}(\zeta _\ell , \mathbf {x}_{[0,{n-1}]}, t_j) \right) \right) \right) \end{aligned}$$

(5.17)

Grouping the $\alpha (n)$ terms:

$$\begin{aligned} = \min (\varphi (n), \max \left( \alpha (n), \underline{\displaystyle \min _{t_j \in [t_i,t_n]}\displaystyle \max _{\ell \in [1,k]}\min (\beta _\ell (n),\rho _{\mathrm{nom}}(\zeta _\ell , \mathbf {x}_{[0,{n-1}]}, t_j))}\right) \end{aligned}$$

(5.18)

Let $\zeta ^j_\ell$ be the shorthand for $\rho _{\mathrm{nom}}(\zeta _\ell ,\mathbf {x}_{[0,{n-1}]},t_j)$. We can rewrite the underlined term in Eq. (5.18) as follows:

$$\begin{aligned} \displaystyle \min _{t_j\in [t_i,t_{n-1}]} \left( \begin{array}{l} \max \left( \min \left( \beta _1, \zeta ^i_1\right) , \ldots , \min \left( \beta _k,\zeta ^i_k\right) \right) , \\ \max \left( \min \left( \beta _1, \zeta ^{i+1}_1\right) , \ldots , \min \left( \beta _k,\zeta ^{i+1}_k\right) \right) , \\ \ldots \\ \max \left( \min \left( \beta _1, \zeta ^{n-1}_1\right) , \ldots , \min \left( \beta _k,\zeta ^{n-1}_k\right) \right) \end{array} \right) \end{aligned}$$

(5.19)

Since $\min$ and $\max$ are distributive over each other, we can now repeatedly apply the rule $\min (\max (a,b), \max (c,d))$ = $\max ( \min (a,c), \min (a,d), \min (b,c), \min (b,d))$ to the above expression. Observe that this will lead to an expression representing a $\max$ over an exponential number of terms. What will these terms look like? There will be $\left( {\begin{array}{c}k\\ 1\end{array}}\right)$ terms of the form $\min (\beta _\ell , \zeta _\ell ^i, \zeta _\ell ^{i+1}, \zeta _\ell ^{n-1})$. This is equivalent to $\min (\beta _\ell , \rho _{\mathrm{nom}}(\Box (\zeta _\ell ), \mathbf {x}_{[0,{n-1}]}, t_i))$. Then, there will be $\left( {\begin{array}{c}k\\ 2\end{array}}\right)$ terms of the form:

$$\begin{aligned} \min \left( \beta _\ell ,\beta _m, \displaystyle \max _{A \in \Pi _{j=1}^{n-1} \{\zeta _\ell ^j,\zeta _m^j\}} \min A\right) . \end{aligned}$$

In the above expression the set A is an element of the $n-i$-fold Cartesian product of $\{\zeta _\ell ^j,\zeta _m^j\}$. Note that there are $2^{n-i}$ elements in the Cartesian product. The reader can verify that this expression is actually equivalent to $\min (\beta _\ell ,\beta _m, \displaystyle \min _{j\in [i,n-1]} \max (\zeta _\ell ^j,\zeta _m^j))$. This in turn simplifies to $\min (\beta _\ell ,\beta _m, \rho _{\mathrm{nom}}(\Box (\zeta _\ell \vee \zeta _m), \mathbf {x}_{[0,{n-1}]}, t_i))$. We can continue this process considering terms that group three $\beta$ values together, four $\beta$ values, and so on. We can show that this results in expression (5.20) below. In this expression, K denotes [1, k] (i.e., the set $\{1,\ldots ,k\}$). For convenience, let $\left( {\begin{array}{c}K\\ \ell \end{array}}\right)$ denote the set of all $\ell$ element combinations of the set K. E.g., if $k = 3$, i.e., $K = \{1,2,3\}$, $\left( {\begin{array}{c}K\\ 2\end{array}}\right)$ = $\{(1,2), (2,3), (3,1)\}$.

$$\begin{aligned} \displaystyle \max _{m\in K} \displaystyle \max _{L \in \left( {\begin{array}{c}K\\ m\end{array}}\right) } \min \left( \left( \displaystyle \min _{\ell \in L} \beta _\ell \right) , \rho _{\mathrm{nom}}\left( \Box \left( \bigvee _{\ell \in L} \zeta _\ell \right) , \mathbf {x}_{[0,{n-1}]}, t_i\right) \right) \end{aligned}$$

(5.20)

We can now substitute expression (5.20) in Eq. (5.18) and using the rule $\min (a,\max (b,c))$ = $\max (\min (a,b), \min (a,c))$, we get an expression that is of the form specified in Eq. (5.3):

$$\begin{aligned} E\left( \begin{array}{l} t_i, \min (\varphi (n),\alpha (n)), \\ \left( \begin{array}{l} \displaystyle \min _{\ell \in L} \min (\varphi (n), \beta _\ell (n)), \\ \Box \left( \bigvee _{\ell \in L}\zeta _\ell \right) \end{array} \right) _{\forall L \in \left( {\begin{array}{c}K\\ 1\end{array}}\right) }, \ldots , \left( \begin{array}{l} \displaystyle \min _{\ell \in L} \min (\varphi (n), \beta _\ell (n)), \\ \Box \left( \bigvee _{\ell \in L}\zeta _\ell \right) \end{array} \right) _{\forall L \in \left( {\begin{array}{c}K\\ k\end{array}}\right) } \end{array} \right) . \end{aligned}$$

(5.21)

The total number of terms in the above expression is $\sum _{m=1}^k \left( {\begin{array}{c}k\\ m\end{array}}\right)$, i.e., $2^k$. Thus, if the expression for $\varphi$ has k summary variables, the expression for $\Box \varphi$ can require up to $2^k$ summary variables. $\square$

Example 2

As the formula for $\Box \varphi$ is hard to parse, consider the following example for the expression corresponding to (5.20) for the case when $k=3$, i.e., when the exression representing the nominal robustness of $\varphi$ has three $(\beta ,\zeta )$ pairs:

$$\begin{aligned} \max \left( \begin{array}{l} \min (\beta _1(n), \rho _{\mathrm{nom}}(\Box \zeta _1, \mathbf {x}_{[0,{n-1}]}, t_i)), \\ \min (\beta _2(n), \rho _{\mathrm{nom}}(\Box \zeta _2, \mathbf {x}_{[0,{n-1}]}, t_i)), \\ \min (\beta _3(n), \rho _{\mathrm{nom}}(\Box \zeta _3, \mathbf {x}_{[0,{n-1}]}, t_i)), \\ \min (\min (\beta _1(n),\beta _2(n)), \rho _{\mathrm{nom}}(\Box (\zeta _1\vee \zeta _2), \mathbf {x}_{[0,{n-1}]}, t_i)), \\ \min (\min (\beta _1(n),\beta _3(n)), \rho _{\mathrm{nom}}(\Box (\zeta _1\vee \zeta _3), \mathbf {x}_{[0,{n-1}]}, t_i)), \\ \min (\min (\beta _2(n),\beta _3(n)), \rho _{\mathrm{nom}}(\Box (\zeta _2\vee \zeta _3), \mathbf {x}_{[0,{n-1}]}, t_i)), \\ \min (\min (\beta _1(n),\beta _2(n),\beta _3(n)), \rho _{\mathrm{nom}}(\Box (\zeta _1\vee \zeta _2\vee \zeta _3), \mathbf {x}_{[0,{n-1}]}, t_i)) \end{array} \right) \end{aligned}$$

(5.22)

Lemma 7

The nominal robustness of $\varphi \mathbf {U}\varphi _2$ at time $t_i \in [t_0,t_{n-1}]$ for the partial signal $\mathbf {x}_{[0,{n}]}$ can be written as an expression of the form (5.3).

Proof

By the definition of nominal robustness:

$$\begin{aligned} \rho _{\mathrm{nom}}(\varphi _1\mathbf {U}\varphi _2,\mathbf {x}_{[0,{n}]}, t_i) = \displaystyle \max _{t_j \in [t_i,t_n]}\min \left( \begin{array}{l} \displaystyle \min _{t_h \in [t_i,t_j]} \rho _{\mathrm{nom}}(\varphi _1, \mathbf {x}_{[0,{n}]}, t_h), \\ \rho _{\mathrm{nom}}(\varphi _2, \mathbf {x}_{[0,{n}]}, t_j) \end{array} \right) \end{aligned}$$

(5.23)

Separating the computation for time $t_n$ in the outermost $\max$ operation:

$$\begin{aligned} = \max \left( \begin{array}{l} \min \left( \varphi _2(n), \varphi _1(n), \underline{\displaystyle \min _{t_h \in [t_i,t_{n-1}]} \rho _{\mathrm{nom}}(\varphi _1, \mathbf {x}_{[0,{n}]}, t_h) }\right) , \\ \displaystyle \max _{t_j \in [t_i,t_{n-1}]} \min \left( \begin{array}{l} \displaystyle \min _{t_h \in [t_i,t_j]} \rho _{\mathrm{nom}}(\varphi _1, \mathbf {x}_{[0,{n}]}, t_h), \\ \rho _{\mathrm{nom}}(\varphi _2, \mathbf {x}_{[0,{n}]}, t_j) \end{array} \right) \end{array} \right) \end{aligned}$$

(5.24)

Observe that the underlined term in the above expression, is equivalent to $\rho _{\mathrm{nom}}(\Box \varphi _1, \mathbf {x}_{[0,{n-1}]}, t_i)$. We now analyze term in the second line of the above expression, i.e.,

$$\begin{aligned} \displaystyle \max _{t_j\in [t_i,t_{n-1}]} \min \left( \begin{array}{l} \rho _{\mathrm{nom}}(\varphi _2, \mathbf {x}_{[0,{n}]}, t_j), \\ \displaystyle \min _{t_h \in [t_i,t_j]} \rho _{\mathrm{nom}}(\varphi _1, \mathbf {x}_{[0,{n}]}, t_h) \end{array} \right) . \end{aligned}$$

(5.25)

From the inductive hypothesis, we can write $\rho _{\mathrm{nom}}(\varphi _1,\mathbf {x}_{[0,{n}]},t_h) = \max (\alpha ^1(n), A_h)$, where:

$$\begin{aligned} A_h = \displaystyle \max _{\ell \in [1,k_1]} \min \left( \beta ^{1}_\ell (n), \rho _{\mathrm{nom}}\left( \zeta ^1_\ell , \mathbf {x}_{[0,{n-1}]},t_h\right) \right) \end{aligned}$$

Similarly, we can write $\rho _{\mathrm{nom}}(\varphi _2, \mathbf {x}_{[0,{n}]}, t_j)$ = $\max (\alpha ^2(n), B_j)$. Then, expression (5.25) can be written as:

$$\begin{aligned} \max \left( \begin{array}{l} \min \left( \max \left( \alpha ^2(n), B_i\right) ,\max \left( \alpha ^1(n),A_i\right) \right) , \\ \min \left( \max \left( \alpha ^2(n), B_{i+1}\right) , \max \left( \alpha ^1(n), A_i\right) , \max \left( \alpha ^1(n), A_{i+1}\right) \right) , \\ \min \left( \max \left( \alpha ^2(n), B_{n-1}\right) , \min \left( \max \left( \alpha ^1(n), A_i\right) ,\ldots ,\max \left( \alpha ^1(n),A_{n-1}\right) \right) \right) \end{array}\right) \end{aligned}$$

(5.26)

We can rewrite the hth row of expression (5.26) as follows:

$$\begin{aligned} \min \left( \max \left( \alpha ^2(n),B_j\right) ,\max \left( \alpha ^1(n), \displaystyle \min _{h\in [i,j]} A_h\right) \right) . \end{aligned}$$

(5.27)

We use the equivalence $\displaystyle \min _{h \in [i,j]} \max \left( \alpha ^1, A_h\right) = \max \left( \alpha ^1, \displaystyle \min \nolimits _{j\in [i,n]} A_h\right)$ for the above rewriting. Distributing the $\min$ operation over the $\max$ operations in expression (5.27), we get:

$$\begin{aligned} \max \left( \begin{array}{ll} \min \left( \alpha ^2(n),\alpha ^1(n)\right) ,&{} \min \left( \alpha ^2(n), \displaystyle \min _{h\in [i,j]} A_h\right) , \\ \min \left( B_j, \alpha ^1(n)\right) ,&{} \min \left( B_j, \displaystyle \min _{h\in [i,j]} A_h\right) \end{array}\right) . \end{aligned}$$

(5.28)

Substituting the above in Eq. (5.26), and grouping similar terms together, we get:

(5.29)

The underlined expression above is equivalent to $A_i$. The expression with the squiggly underline reduces to the following expression:

$$\begin{aligned} \displaystyle \max _{m\in [1,k_2]}\Big (\min \left( \alpha ^1(n), \beta _m^2(n), \rho _{\mathrm{nom}}\left( \Diamond \zeta ^2_m, \mathbf {x}_{[0,{n-1}]}, t_i\right) \right) \Big ). \end{aligned}$$

(5.30)

We are then left with the term that has the dashed underline. Substituting the expressions for $B_j$ and $A_h$, we get:

$$\begin{aligned} \displaystyle \max _{j \in [i,n-1]} \min \left( \begin{array}{l} \displaystyle \max _{m \in [1,k_2]} \min \left( \beta _m^2(n), \zeta _m^{2,j}\right) , \\ \displaystyle \min _{h \in [i,j]} \displaystyle \max _{\ell \in [1,k_1]} \min \left( \beta _\ell ^1(n), \zeta _\ell ^{1,h}\right) \end{array}\right) \end{aligned}$$

(5.31)

We can expand this formula over the outermost j index, and start grouping terms in a fashion similar to the technique in the proof of Lemma (6). We can show that we get an expression of the following form:

$$\begin{aligned} \max \left( \begin{array}{l} \displaystyle \max _{\begin{array}{c} m\in [1,k_2] \\ \ell \in [1,k_1] \end{array}} \min \left( \beta ^2_m(n), \beta ^1_\ell (n), \rho _{\mathrm{nom}}\left( \zeta ^1_\ell \mathbf {U}\zeta ^2_m,\mathbf {x}_{[0,{n-1}]},t_i\right) \right) , \\ \displaystyle \max _{\begin{array}{c} m\in [1,k_2] \\ \ell _1 \in [1,k_1] \\ \ell _2 \in [1,k_1] \end{array}} \min \left( \beta ^2_m(n), \beta ^1_{\ell _1}(n), \beta ^1_{\ell _2}(n), \rho _{\mathrm{nom}}\left( \left( \zeta ^1_{\ell _1} \vee \zeta ^1_{\ell _2}\right) \mathbf {U}\zeta ^2_m, \mathbf {x}_{[0,{n-1}]}, t_i\right) \right) , \\ \qquad \ldots , \ldots , \\ \displaystyle \max _{m\in [1,k_2]} \min \left( \beta ^2_m(n), \displaystyle \min _{\ell \in [1,k_1]} \beta ^1_\ell (n), \rho _{\mathrm{nom}}\left( \left( \bigvee _{\ell \in [1,k_1]} \zeta ^1_\ell \right) \mathbf {U}\zeta ^2_m, \mathbf {x}_{[0,{n-1}]}\right) \right) \end{array}\right) \end{aligned}$$

(5.32)

We can now substitute expressions (5.30) and (5.32) in expression (5.29), and then substitute the second term in Eq. (5.24) with the resulting expression, we get the following expression for the nominal robustness for $\varphi _1 \mathbf {U}\varphi _2$:

$$\begin{aligned} E\left( \begin{array}{l} t_i, \min \left( \alpha ^1(n),\alpha ^2(n)\right) , \\ \left( \varphi _2(n),\ \Box \varphi _1\right) , \\ \left( \min \left( \beta ^2_m(n),\alpha ^1(n)\right) ,\ \Diamond \zeta ^2_m\right) _{m \in [1,k_2]}, \\ \left( \min \left( \beta ^2_m(n), \min _{\ell \in L} \beta ^1_\ell (n)\right) ,\ \left( \bigvee _{\ell \in L} \zeta ^1_\ell \right) \mathbf {U}\zeta ^2_m\right) _{\{L \in \left( {\begin{array}{c}K_1\\ r\end{array}}\right) \mid r\in K_1\}, m \in [1,k_2]} \end{array}\right) \end{aligned}$$

(5.33)

Observe that if $\varphi _1$ and $\varphi _2$ have respectively $k_1$ and $k_2$ summary variables, then the nominal robustness for $\varphi _1 \mathbf {U}\varphi _2$ needs $k_2 + k_2\cdot 2^{k_1}$ summary variables. $\square$

Lemma 8

The nominal robustness of $\varphi \mathbf {R}\varphi _2$ at time $t_i \in [t_0,t_{n-1}]$ for the partial signal $\mathbf {x}_{[0,{n}]}$ can be written as an expression of the form (5.3).

Proof

The proof for the $\mathbf {R}$ operator is very similar to that of the $\mathbf {U}$ and the $\Box$ operator. For brevity, we omit the tedious steps required to show that the expression for nominal robustness for $\varphi _1 \mathbf {R}\varphi _2$ can be written as:

$$\begin{aligned} E\left( \begin{array}{l} t_i, \min \left( \varphi _2(n),\alpha ^2(n)\right) , \\ \left( \min \left( \varphi _2(n),\displaystyle \min _{m \in M} \beta ^2_m(n)\right) ,\ \Box \left( \bigvee _{m \in M} \zeta ^2_m\right) \right) , \\ \left( \displaystyle \min _{m \in M} \beta ^2_m(n),\ \Diamond \varphi _1 \wedge \Box \left( \bigvee _{m \in M} \zeta ^2_m\right) \right) , \\ \left( \min \left( \displaystyle \min _{m \in M} \beta _\ell ^2(n), \displaystyle \min _{\ell \in L} \beta _\ell ^1(n), \varphi _2(n)\right) ,\ \left( \bigvee _{\ell \in L} \zeta ^1_\ell \right) \mathbf {R}\left( \bigvee _{m \in M} \zeta ^2_m\right) \right) , \\ \left( \min \left( \displaystyle \min _{m \in M} \beta _\ell ^2(n), \displaystyle \min _{\ell \in L} \beta _\ell ^1(n)\right) ,\ \Diamond \varphi _1 \wedge \left( \bigvee _{\ell \in L} \zeta ^1_\ell \right) \mathbf {R}\left( \bigvee _{m \in M} \zeta ^2_m\right) \right) , \\ \left( \varphi _2(n),\ \varphi _1\right) , \left( +\infty ,\ \Diamond \varphi _1\right) \\ \end{array}\right) \end{aligned}$$

(5.34)

In the above expression, for the second and third lines, M is an element of $\left( {\begin{array}{c}K_2\\ r\end{array}}\right)$, for every $r \in K_2$. For the fourth and fifth lines, M is an element of $\left( {\begin{array}{c}K_2\\ r\end{array}}\right)$, for every r in $K_2$, and L is an element of $\left( {\begin{array}{c}K_1\\ r\end{array}}\right)$ for every r in $K_1$. Observe that if $\varphi _1$ and $\varphi _2$ have respectively $k_1$ and $k_2$ summary variables, then the nominal robustness for $\varphi _1 \mathbf {R}\varphi _2$ requires $2^{k_1 + k_2} + 2^{k_2} + 1$ summary variables. $\square$

Theorem 1

The robust satisfaction interval for any formula $\varphi$ belonging to the syntactic fragment STL_u can be monitored in an online fashion using a fixed amount of memory that depends on a function of $|\varphi |$ where $|\varphi |$ indicates the length of $\varphi$, and independent of the trace length.

Proof

The proof follows from the proofs of Lemmata 2, 3, 4, 5, 6, 7 and 8. Substituting $t_i = 0$ in the expression for nominal robustness of the top-level formula. Note that any subformula with top-level operators $\mathbf {U}$ or $\Box$ requires memory that is exponential in the number of variables required to monitor its subformulae. However, the memory required is independent of trace-length, and dependent only on the size of the formula. $\square$

We now give a couple of examples to show how the lemmata in the above proof can be applied to obtain an algorithmic procedure to monitor STL_u formulae.

Example 3

Consider the formula $\Box \Diamond (x>0)$. Applying Lemma 2, the nominal robustness for $x>0$ is:

$$\begin{aligned} E\left( t_i, -\infty , (+\infty , x>0)\right) \end{aligned}$$

(5.35)

From Lemma 5, the nominal robustness for $\Diamond (x>0)$ is:

$$\begin{aligned}&E\left( t_i, \max (-\infty , x(n)), (+\infty , \Diamond (x>0))\right) \nonumber \\&\quad =E\left( t_i, x(n), \min (+\infty , \Diamond (x>0))\right) \end{aligned}$$

(5.36)

From Lemma 6, we can write the nominal robustness for $\Box \Diamond (x>0)$:

$$\begin{aligned} E\left( \begin{array}{l} t_i, \max (x(n),x(n)), \\ \left( \min (x(n), +\infty ),\ \Box \Diamond (x>0)\right) \end{array}\right) \end{aligned}$$

(5.37)

We can see that above expression simplies to simply x(n). In other words, nominal robustness of $\Box \Diamond (x>0)$ depends only on the value of x(t) at time $t_n$.

Example 4

Consider the formula $\Box \left( (x>0) \vee \Diamond (y>0)\right)$. Applying Lemma 2, the nominal robustness for the formula $(y>0)$ is the following expression:

$$\begin{aligned} E\left( t_i, -\infty , (+\infty , y>0)\right) \end{aligned}$$

(5.38)

From Lemma 5, we can write the nominal robustness for formula $\Diamond (y>0)$ as follows:

$$\begin{aligned}&E\left( t_i, \max (-\infty , y(n)), (+\infty , \Diamond (y>0))\right) \nonumber \\&\quad =E\left( t_i, y(n), \min (+\infty , \Diamond (y>0))\right) \end{aligned}$$

(5.39)

Similar to (5.38), the nominal robustness for $(x>0)$ is $E\left( t_i, -\infty , (+\infty , x))\right)$. From Lemma 4, we can write the nominal robustness for $(x>0) \vee \Diamond (y>0)$ as:

$$\begin{aligned}&E\left( t_i, \max (-\infty , y(n)), (+\infty , x>0), (+\infty , \Diamond (y>0)) \right) \nonumber \\&\quad =E\left( t_i, y(n), (+\infty , x>0), (+\infty , \Diamond (y>0))\right) \end{aligned}$$

(5.40)

Finally, using Lemma (6), the nominal robustness for $\Box ( (x>0) \vee \Diamond (y>0) )$ at time 0 can be written as:

$$\begin{aligned} E\left( \begin{array}{l} 0, \min (\max (x(n),y(n)), y(n)), \\ \left( \min (+\infty , \max (x(n),y(n))),\ \Box (x>0)\right) , \\ \left( \min (+\infty , \max (x(n),y(n))),\ \Box (\Diamond (y>0))\right) , \\ \left( \min (+\infty , \max (x(n),y(n))),\ \Box (x>0 \vee \Diamond (y>0))\right) \end{array} \right) \end{aligned}$$

(5.41)

From Example 3, we can see that $\rho _{\mathrm{nom}}(\Box (\Diamond (y>0)), \mathbf {x}_{[0,{n-1}]}, 0)$ is $y(n-1)$, so the above expression simplifies to:

$$\begin{aligned} \max \left( \begin{array}{l} y(n), \min (\max (x(n),y(n)), \rho _{\mathrm{nom}}(\Box (x>0),\mathbf {x}_{[0,{n-1}]},0)), \\ \min (\max (x(n),y(n)),y(n-1)), \\ \min (\max (x(n),y(n)), \rho _{\mathrm{nom}}(\Box (x>0 \vee \Diamond (y>0)), \mathbf {x}_{[0,{n-1}]}, 0)) \\ \end{array} \right) \end{aligned}$$

(5.42)

This shows that we can monitor the nominal robustness of $\Box (x>0 \vee \Diamond (y>0)))$ using two variables (one for $\Box (x>0)$ and one for $\Box (x>0 \vee \Diamond (y>0))$). In the case of this formula, we can show that this can be further simplified to:

$$\begin{aligned} \max (y(n), \min (x(n), \rho _{\mathrm{nom}}(\Box (x>0 \vee \Diamond (y>0)), \mathbf {x}_{[0,{n-1}]}, 0))). \end{aligned}$$

(5.43)

This allows us to monitor the formula with just one variable.

Example 5

Consider the formula $\Diamond ( (x>0) \wedge \Diamond (y>0) )$. The expressions for nominal robustness of $\Diamond (y>0)$ and $x>0$ are as in (5.39) and (5.35) respectively. From Lemma (3), the expression for $(x>0) \wedge \Diamond (y>0)$ is:

$$\begin{aligned} E\left( \begin{array}{l} t_i, \min (-\infty , y(n)), \\ \left( \min (-\infty , +\infty ),\ \Diamond (y>0)\right) \\ \left( \min (y(n), +\infty ),\ x>0\right) \\ \left( \min (+\infty ,+\infty ),\ (x>0) \wedge \Diamond (y>0)\right) \end{array} \right) \end{aligned}$$

(5.44)

We can drop the second line in the above expression, as it corresponds to a $\min$ with $-\infty$ as an argument. The above expression then simplifies to:

$$\begin{aligned} E\left( t_i, -\infty ,\ \ \left( y(n),\ x>0\right) ,\ \ \left( +\infty ,\ (x>0) \wedge \Diamond (y>0)\right) \right) . \end{aligned}$$

(5.45)

Now, applying Lemma 5 again, we get the following expression:

$$\begin{aligned} E\left( \begin{array}{l} 0, -\infty , \\ \left( y(n),\ \Diamond (x>0)\right) , \\ \left( +\infty ,\ \Diamond (x>0 \wedge \Diamond (y>0))\right) \end{array} \right) \end{aligned}$$

(5.46)

This simplifies to the following expression:

$$\begin{aligned} \max \left( \begin{array}{l} \min (y(n), \rho _{\mathrm{nom}}(\Diamond (x>0), \mathbf {x}_{[0,{n-1}]}, 0)), \rho _{\mathrm{nom}}(\Diamond ((x>0) \wedge \Diamond (y>0)), \mathbf {x}_{[0,{n-1}]}, 0) \end{array} \right) . \end{aligned}$$

Thus, the formula $\Diamond (x>0 \wedge \Diamond (y>0))$ can be monitored using two variables, one for the value of $\Diamond (x>0)$ till time $t_{n-1}$ and one for $\Diamond ((x>0) \wedge \Diamond (y>0))$ till time $t_{n-1}$.

5.4 Extension to full STL

To extend the results from STL_u to STL, we need to perform certain steps. First, we recall a result from [11], which shows that any Metric Temporal Logic formula can be rewritten as a formula in which no unbounded time-horizon temporal operator appears in the scope of a bounded horizon temporal operator.

Example 6

Consider the formula $\Diamond _{[0,2]} \Box (x > 0)$. Following the rewrite rules from [11], we can rewrite this formula as: $(\Diamond _{[0,2]} \Box _{[0,2]} (x>0)) \wedge \Box (\tilde{x}>0)$, where $\tilde{x}$ is the signal x delayed by 2 time units.

We can now extend Theorem 1 to allow subformulae that are not just atomic predicates, but timed temporal operators. The key idea is to use a syntax tree similar to that for online monitoring of the bounded horizon STL formulae as in Sect. 4. For formulas containing unbounded horizon STL formulas, a naïve version of the algorithm would require an infinite number of elements to be stored in the worklists at each node in the tree. However, by observing that we can summarize computation on partial signals in variables, we can monitor STL formulas using a finite amount of memory.

For any unbounded horizon temporal formula, suppose the maximum time horizon of the bounded horizon subformulas is h. Given a partial signal from time $t_0$ to $t_n$, we can use the techniques from Theorem 1 without modification to monitor the nominal robustness till time $t_n - h$. For the last h time units, we cannot compute the exact robustness values of the bounded horizon temporal formulas. For each time-point in the interval $[t_n -h, t_n]$, we can maintain a tree with worklists similar to Algorithm 2 to monitor the bounded horizon subformula. Note that due to the minimum time-step stipulation, we need to maintain only a finite number of such trees. Thus, unlike the case for STL_u where the computation of nominal robustness over the partial signal $\mathbf {x}_{[0,{n}]}$ can be expressed in terms of a summary value over the partial signal $\mathbf {x}_{[0,{n-1}]}$, and the signal value at time $t_n$, in case of full STL, the computation is expressed as computation over the partial signal over $[0,t_n-h]$, and a finite number of trees for the bounded horizon subformulae (which contain the signal values in $[t_n-h, t_n]$. We omit the precise details for brevity.

6 Experimental results

We implemented Algorithm 2 as part of two independant tools: Breach [4], and CPSGrader [16]. Breach is a Matlab toolbox with a strong focus on monitoring and analysis of Simulink models [20], though simple wrappers can be used to make it usable with other simulators or real time measured data. CPSGrader is a C++ library. Both tools support full STL specifications. In the following, we illustrate the use of online monitoring with the benchmark model proposed in [14], then evaluate it on two case studies. We considered the following criteria: (1) On an average, what fraction of simulation time can be saved by online monitoring? (2) How much overhead does online monitoring add, and how does it compare to a naïve implementation that at each step recomputes everything using an offline algorithm?

6.1 Fuel control model

The model presented in Fig. 4 is a subsystem of gasoline engine implemented in Simulink. Its purpose is to control the engine air-fuel (AF) ratio so as to meet emissions targets, an important control functionality in a gasoline engine. The model contains the air-fuel controller and a mean value model of the engine dynamics, such as the throttle and intake manifold air dynamics. Inputs of this system model are PedalAngle and EngineSpeed. Outputs are AF, AFref and controller Mode. Typical properties to verify and monitor are overshoot and settling time.

Fig. 4

Abstract Fuel Control model test harness augmented with an online monitoring block. Details of the model can be found in the given reference [14]

To illustrate the use of online monitoring in Simulink, we augmented the test harness with an STL monitoring block available in Breach. The block, depicted in Fig. 5, accepts arbitrary STL formulas on its input signals and outputs a two dimensional signals computing the robust interval. It can be configured to stop simulation whenever the robust interval becomes positive, negative or singular,i.e., when no uncertainty remain in the eventual value of robust satisfaction.

Fig. 5

Details of the online monitoring block for the Abstract Fuel Control model and formula 6.1

We ran the model with the following formula:

$$\begin{aligned} \varphi _\text {AFC} = \Box _{[10,30]}(\left| \text {AF}-\text {AFref}\right| > 0.1\! \implies \!\!(\Diamond _{[0, 5]}\!\left| \text {AF}-\text {AFref}\right| < 0.1 )) \end{aligned}$$

(6.1)

The resulting signals, AF, AFref and lower and upper robustness are depicted on Fig. 6. It shows the reduction of robust interval as time advances, until the full determination of its sign and value, before the expected horizon of the formula.

Fig. 6

Output of a simulation and online computation of lower and upper bounds of robustness for the fuel control model. Note that in this example, we set the maximum interval robustness to $[-0.5, 0.5]$. In this run, simulation could have been stopped early shortly after $\hbox {t}=30~\hbox {s}$, when interval robustness becomes positive, or at $\hbox {t}=33.5~\hbox {s}$ when the interval becomes singular, i.e., robust satisfaction is deterministically known. Note that the horizon of the formula is 35 s. (Color figure online)

Next, we proceed with a more systematic evaluation of online monitoring performance on two case studies.

6.2 Diesel engine model (DEM)

The first case study is an industrial-sized Simulink^®model of a prototype airpath system in a diesel engine. The closed-loop model consists of a plant model describing the airpath dynamics, and a controller implementing a proprietary control scheme. The model has more than 3000 blocks, with more than 20 lookup tables approximating high-dimensional nonlinear functions. Due to the significant model complexity, the speed of simulation is about 5 times slower, i.e., simulating 1 s of operation takes 5 s in Simulink^®. As it is important to simulate this model over a long time-horizon to characterize the airpath behavior over extended periods of time, savings in simulation-time by early detection of requirement violations is very beneficial. We selected two parameterized safety requirements after discussions with the control designers, (shown in Eq. (6.2)–(6.3)). Due to proprietary concerns, we suppress the actual values of the parameters used in the requirements.

$$\begin{aligned} \varphi _{ overshoot }(\mathbf {p_1})= & {} \Box _{[a,b]}(\mathbf {x}< c) \end{aligned}$$

(6.2)

$$\begin{aligned} \varphi _{ transient }(\mathbf {p_2})= & {} \Box _{[a,b]}(\left| \mathbf {x}\right| > c\! \implies \!\!(\Diamond _{[0, d]}\!\left| \mathbf {x}\right| < e )) \end{aligned}$$

(6.3)

Property $\varphi _{ overshoot }$ with parameters $\mathbf {p_1} = (a,b,c)$ specifies that in the interval [a, b], the overshoot on the signal $\mathbf {x}$ should remain below a certain threshold c. Property $\varphi _{ transient }$ with parameters $\mathbf {p_2} = (a,b,c,d,e)$ is a specification on the settling time of the signal $\mathbf {x}$. It specifies that in the time interval [a, b] if at some time t, $\left| \mathbf {x}\right|$ exceeds c then it settles to a small region ($\left| \mathbf {x}\right| < e$) before $t+d$. In Table 1, we consider three different valuations $\nu _1$, $\nu _2$, $\nu _3$ for $\mathbf {p_1}$ in the requirement $\varphi _{ overshoot }(\mathbf {p_1})$, and two different valuations $\nu _4$, $\nu _5$ for $\mathbf {p_2}$ in the requirement $\varphi _{ transient }(\mathbf {p_2})$.

The main reason for the better performance of the online algorithm is that simulations are time-consuming for this model. The online algorithm can terminate a simulation earlier (either because it detected a violation or obtained a concrete robust satisfaction interval), thus obtaining significant savings. For $\varphi _{ overshoot }(\nu _3)$, we choose the parameter values for a and b such that the online algorithm has to process the entire signal trace, and is thus unable to terminate earlier. Here we see that the total overhead (in terms of runtime) incurred by the extra book-keeping by Algorithm 2 is negligible (about 0.1%).

Table 1 Experimental results on DEM

6.3 CPSGrader

CPSGrader [6, 16] is a publicly-available automatic grading and feedback generation tool for online virtual labs in cyber-physical systems. It employs temporal logic based testers to check for common fault patterns in student solutions for lab assignments. CPSGrader uses the National Instruments Robotics Environment Simulator to generate traces from student solutions and monitors STL properties (each corresponding to a particular faulty behavior) on them. In the published version of CPSGrader [16], this is done in an offline fashion by first running the complete simulation until a pre-defined cut-off and then monitoring the STL properties on offline traces. At a step-size of 5 ms, simulating 6 s of real-world operation of the system takes 1 s for the simulator. When students use CPSGrader for active feedback generation and debugging, simulation constitutes the major chunk of the application response time. Online monitoring helps in reducing the response time by avoiding unnecessary simulations, giving the students feedback as soon as faulty behavior is detected.

We evaluated our online monitoring algorithm, on the traces and STL properties used in the published version of CPSGrader [6, 16]. These traces are the result of running actual student submissions on a battery of tests. For lack of space, we refer the reader to [16] for details about the tests and STL properties. As an illustrative example, we show the $\texttt {keep\_bump}$ property in Eq. 6.4:

$$\begin{aligned} \varphi _{\texttt {keep\_bump}}= \Diamond _{[0, 60]} \Box _{[0, 5]}\left( \texttt {bump\_right}(t) \vee \texttt {bump\_left}(t)\right) \end{aligned}$$

(6.4)

This formula encodes the behavior that less than 60 s from the beginning of the simulation, either the right bump sensor or the left bump sensor stays on for at least 5 s, which indicates that the robot is likely stuck against an obstacle.

For each STL property, Table 2 compares the total simulation time needed for both the online and offline approaches, summed over all traces. For the offline approach, a suitable simulation cut-off time of 60 s is chosen. At a step-size of 5 ms, each trace is roughly of length 1000. For the online algorithm, simulation terminates before this cut-off if the truth value of the property becomes known, otherwise it terminates at the cut-off. Table 2 also shows the monitoring overhead incurred by a naïve online algorithm that performs complete recomputation at every step against the overhead incurred by Algorithm 2. Table 2 demonstrates that online monitoring ends up saving up to 24% simulation time (>10% in a majority of cases). The monitoring overhead of Algorithm 2 is negligible (<1%) as compared to the simulation time and it is less than the overhead of the naïve online approach consistently by a factor of 40–80x.

Table 2 Evaluation of online monitoring for CPSGrader

7 Conclusion

STL is a convenient and versatile specification language for monitoring complex requirements or specifications for CPS. Its robust semantics provides information complementing the usual Boolean Yes/No satisfaction answer that can be instrumental at the design, verification or runtime phase. Being able to compute it online, i.e., as simulations or the actual system run, is thus a highly desirable feature, for which this paper proposes an efficient and sound solution. The key idea is the concept of interval robustness, which provides conservative bounds for the robust satisfaction of a formula by a behavior at all time instants. We showed how robust intervals can be computed efficiently and using only bounded memory. As future work, we will propose and implement new algorithms for monitoring piecewise linear signals specified and investigate other quantitative semantics, e.g., as in [22], and possible efficient hardware implementations based on FPGA, in the spirit of [13].