## 2 Signal Temporal Logic  
Signal temporal logic (STL) [3] is a linear-time temporal logic designed as a formal specification language for classifying the time-dependent signals originating from continuous-state or hybrid-state dynamical systems. Its development has been motivated by a need for a flexible yet rigorous language systematising the monitoring of cyber-physical systems. Especially relevant to such monitoring applications is the bounded-time fragment of STL defined as follows. Definition 1: Formulae \(\phi\) of _bounded-time STL_ are defined by the Backus-Naur form  
\[\phi := \top\mid g\geq c\mid\
eg\phi\mid\phi\vee\phi\mid\phi\mathbf{U}_{[t,t]}\phi\] \[g := cx\mid cx+g\] \[c :\in \mathbb{Q}\] \[x := \mathit{Var}\] \[t :\in \mathbb{N}\]  
where \(\mathit{Var}\) is a predefined set of signal names. We demand that \(t\leq t^{\prime}\) in \(\mathbf{U}_{[t,t^{\prime}]}\phi\). The constant \(\bot\), further Boolean connectives like \(\wedge\) or \(\Rightarrow\), and further modalities \(\mathbf{F}_{[t,t]}\phi\) or \(\mathbf{G}_{[t,t]}\phi\) can be defined as usual: for example, \(\mathbf{F}_{[t,t^{\prime}]}\phi\) is an abbreviation for \(\top\mathbf{U}_{[t,t^{\prime}]}\phi\) and \(\mathbf{G}_{\leq t}\phi\) is an abbreviation for \(\phi\mathbf{U}_{[t+1,t+1]}\top\) given the discrete nature of the time model. Note that the above definition confines state expressions \(g\) to be linear combinations of signals, in contrast to the standard definition [3] of STL, which permits more general state expressions. The reason for adopting this restriction is that it permits exact results in monitoring, whereas more general state expressions can well be treated in our framework by exploiting standard affine-arithmetic approximations [13], yet completeness would be lost due to overapproximations induced by a strife for soundness. For the same reasons, we adopt a discrete-time semantics, as issues of continuous interpolation between time instants of measurements have been addressed before in [17]. Adopting those mechanisms, continuous-time dynamic systems and continuous-time interpretation of STL can be treated as well, yet would again resort to affine approximations at the price of sacrificing exactness of the monitoring algorithm. The semantics of STL builds on the notion of a trajectory:  
Definition 2: A _state valuation_\(\sigma\) is a mapping of signal names \(x\in\mathit{Var}\) to real values, i.e., a function \(\sigma:\mathit{Var}\rightarrow\mathbb{R}\). The set of all state valuations is denoted by \(\Sigma\). A _(discrete time) trajectory_\(\tau:\mathbb{N}\rightarrow\Sigma\) is a mapping from time instants, where time is identified with the natural numbers \(\mathbb{N}\), to state valuations. _Satisfaction of an STL formula \(\phi\) by a (discrete-time) trajectory \(\tau\) at time instant \(t\in\mathbb{N}\), denoted as \(\tau,t\models\phi\), is defined recursively as \begin{tabular}{l l l} \(\tau,t\models\top\) & _holds_, \\ \(\tau,t\models g\geq c\) & _iff_ & \(G(\tau(t))\geq c\), _where_ \(G\) _is the linear function defined by expression_ \(g\)_,_ \\ \(\tau,t\models\
eg\phi\) & _iff_ & \(\tau,t\
ot\models\phi\)_,_ \\ \(\tau,t\models\phi\vee\psi\) & _iff_ & \(\tau,t\models\phi\) _or_ \(\tau,t\models\psi\)_,_ \\ \(\tau,t\models\phi\mathbf{U}_{[t_{1},t_{2}]}\psi\) & _iff_ & \(\exists k\in\{t+1_{1},\ldots,t+t_{2}\}:(\tau,k\models\psi)\wedge\forall l\in\{t,\ldots,k-1\}:(\tau,l\models\phi)\)_._ \\ \end{tabular}