# Mining Road Traffic Rules with Signal Temporal Logic and Grammar-Based Genetic Programming
## 3 Background: Signal Temporal Logic  
Signal Temporal Logic (STL) is a formal language to specify behaviors of dynamical systems through logic formulas. Let \(\mathcal{X}\) be a set of _trajectories_\(\mathbf{x}:\mathbb{T}\to\mathbb{R}^{p}\) for every \(\mathbf{x}\in\mathcal{X}\), with \(\mathbb{T}\subseteq\mathbb{R}_{\geq 0}\) a time domain. We say that each trajectory is a \(p\)-dimensional _signal_ of real-valued variables, and we denote by \(x_{i}(t)\) the projection on the \(i\)-th coordinate of \(\mathbf{x}=(x_{1},\ldots,x_{p})\) at time \(t\in\mathbb{T}\). We now introduce the _syntax_ of STL, the set of rules used for constructing specifications in this language. **Definition 1** (STL syntax). : _We define the syntax of an STL formula \(\varphi\) using the following grammar:_  
\[\varphi\ :=\ \top\mid\mu\mid\
eg\varphi\mid\varphi_{1}\wedge\varphi_{2}\mid \varphi_{1}\mathsf{S}_{[t_{1},t_{2}]}\varphi_{2}\mid\mathsf{O}_{[t_{1},t_{2}]} \varphi\mid\mathsf{H}_{[t_{1},t_{2}]}\varphi,\]  
_where \(\top\) is the Boolean constant true; \([t_{1},t_{2}]\), with \(t_{1},t_{2}\in\mathbb{T}\), is a time interval such that \(t_{1}<t_{2}\); \(\mu\) is an atomic proposition of the form \(y(t)\sim c\), with \(y:\mathbb{R}^{p}\to\mathbb{R}\) projecting the \(p\)-dimensional signal onto a single variable, \(\sim\in\{<,>\}\) and \(c\in\mathbb{R}^{+}\) being a threshold (practically inequality over the variable of the signal); \(\
eg\) and \(\wedge\) are the usual Boolean connectives; \(\mathsf{S}_{[t_{1},t_{2}]}\) is the Since temporal modality; \(\mathsf{O}_{[t_{1},t_{2}]}\) is the Once temporal modality; and \(\mathsf{H}_{[t_{1},t_{2}]}\) is the Historically temporal modality._  
The _semantics_ of an STL formula \(\varphi\) allows us to tell if and to which degree a trajectory \(\mathbf{x}\) satisfies the formula \(\varphi\) at time \(t\). We now define two kinds of semantics: with the Boolean semantics, the satisfaction assumes Boolean values (does satisfies, does not satisfy); with the quantitative semantics, the satisfaction assumes real-valued values [20,21]. **Definition 2** (STL Boolean Semantics). : _For the Boolean semantics, we write \((\mathbf{x},t)\models\varphi\) if \(\varphi\) holds for trajectory \(\mathbf{x}\) at time \(t\). If \(\varphi\) is an atomic proposition \(\mu\), then \((\mathbf{x},t)\models\varphi\) if and only if \(\mu\) is true. The semantics of \(\
eg\varphi\) and \(\varphi_{1}\wedge\varphi_{2}\) is trivial and the semantics of Since is defined as follows:_  
\[(\mathbf{x},t)\models\varphi_{1}\mathsf{S}_{[t_{1},t_{2}]}\varphi_{2}\ \Leftrightarrow\ \exists\ t^{\prime}<t\ :\ ((\mathbf{x},t^{\prime})\models\varphi_{2}\ \wedge\ \forall\ t^{\prime\prime}\in[t^{\prime},t\big{[}:(\mathbf{x},t^{\prime\prime}) \models\varphi_{1}),\]  
_with \(t^{\prime}\in[t_{1},t_{2}]\). In other words, we say that \(\varphi_{1}\mathsf{S}_{[t_{1},t_{2}]}\varphi_{2}\) is satisfied at time \(t\) if \(\varphi_{2}\) occurs at some point in \([t_{1},t_{2}]\) and \(\varphi_{1}\) holds continuously since then. The other temporal operators are defined based on Since: Once as \(\mathsf{O}_{[t_{1},t_{2}]}\varphi=\top\mathsf{S}_{[t_{1},t_{2}]}\varphi\) and Historically as \(\mathsf{H}_{[t_{1},t_{2}]}\varphi=\
eg\mathsf{O}_{[t_{1},t_{2}]}\
eg\varphi\)._  
**Definition 3** (STL Quantitative Semantics). : _The quantitative satisfaction function \(\rho\) returns a value \(\rho(\varphi,\mathbf{x},t)\in\mathbb{R}\cup\{-\infty,+\infty\}\) quantifying the robustness degree of the formula \(\varphi\) by the trajectory \(\mathbf{x}\) at time \(t\).