Formally, an STL specification can be understood as follows.
Consider a discrete time sequence \(t := \lbrace t_k | k \in \mathbb {Z}_{\geqslant 0}\rbrace \) .
The STL formula \(\varphi \)  is defined using the predicate \(\mu \)  that is of the form \(f(x(t))\) , where \(x(t)\)  is the state of the signal at time \(t\)  and \(f\)  maps each time point to the real-value \(x(t_k)\in \mathbb {R}\) .
The STL syntax is defined as:
\(\varphi \; := \; \mu \; | \; \lnot \varphi \; | \; \varphi _1\wedge \varphi _2 \; | \; \varphi _1\vee \varphi _2 \; | \; \mathbf {G}_{I}\varphi \; | \; \mathbf {F}_{I}\varphi \; | \; \varphi _1 \mathbf {U}_{I}\varphi _2\) .
Where \(I = [a, b]\)  is the set of all \(t_k \in t\)  such that \(a, b \in t\) ; \(b > a \ge 0\) .
The operators \(\lnot , \wedge , \vee \)  refer to Boolean negation, conjunction and disjunction operators respectively.
The temporal operators \(\mathbf {G}, \textbf {F}, \mathbf {U}\)  refer to globally, eventually and until operators, respectively.
A complete definition of STL can be found in [1]},[2]}.
