# Mining Road Traffic Rules with Signal Temporal Logic and Grammar-Based Genetic Programming
## 5 Methodology
### Grammar for STL Formula Structures  
We need to define a grammar \(\mathcal{G}\) for the language of STL formulas. \(\mathcal{G}\) must be customizable for the considered problem, i.e., for its attributes \(A\), and must allow generating formulas along with appropriate values as numerical parameters. In order to favor the building of human-readable formulas, we build the grammar to explicitly limit the depth of nesting of temporal operators. We remark that the overall size of STL formulas is limited by the value of \(d_{\text{max}}\) used by CFGGP (in the operators and in theinitialization of the population). However, we believe that posing a further limit on the composition of the temporal operators may make the STL formulas more readable, and not only just smaller. Our belief is corroborated by the findings of [23] for mathematical expressions: some operators, such as log and sin, make the expressions less interpretable than others, e.g., \(+\) and \(+\). Figure 2 shows the grammar for STL formula structures with limited nesting of the temporal operators. The figure adopts the common Backus-Naur form: the non-terminal symbols are enclosed in angle brackets, whereas the terminal symbols are shown as literals (\(\
eg\), \(\land\),..., \(r\), \(a_{1}\), \(a_{2}\),..., \(<\), \(>\), 0,..., 9); for each non-terminal, derivation rules are separated by \(|\); the starting symbol is the topmost non-terminal, i.e., \(s_{0}=\langle\text{formula}\rangle\). The terminals \(a_{1}\), \(a_{2}\),..., derived from the non-terminal \(\langle\text{attr}\rangle\), represent the attributes of the problem at hand: in this way, the grammar is tailored to a specific problem. For brevity, we express some of the non-terminals using a parameter \(i\) that represents the maximum nesting. The only derivation rule that increases \(i\) is the one for \(\langle\text{temp}_{i}\rangle\), which represents (partial) formulas with temporal operators. The limit to nesting is enforced by the parametric definition of the derivation rule of \(\langle\text{formula}_{i}\rangle\), that does not expand to \(\langle\text{temp}_{i}\rangle\) if \(i\geq i_{\text{max}}\). In this study, we set the maximum nesting to \(i_{\text{max}}=3\). This means that CFGGP operates on a grammar \(\mathcal{G}\) that is the realization of the grammar of Figure 2 with \(i_{\text{max}}=3\) and a given set of attributes \(A\). \[\langle\text{formula}\rangle ::=\langle\text{formula}_{1}\rangle\] \[\langle\text{formula}_{i}\rangle ::= \begin{cases}\langle\text{atom}\rangle\mid\langle\text{logic}_{ i}\rangle\mid\langle\text{temp}_{1}\rangle&\text{if }i<i_{\text{max}}\\ \langle\text{atom}\rangle\mid\langle\text{logic}_{i}\rangle&\text{otherwise} \end{cases} \] \[\langle\text{logic}_{i}\rangle ::=\
eg\langle\text{formula}_{i}\rangle\mid\langle\text{formula}_{ i}\rangle\wedge\langle\text{formula}_{i}\rangle\] \[\langle\text{temp}_{i}\rangle ::=\langle\text{formula}_{i+1}\rangle S\langle\text{interval} \rangle\langle\text{formula}_{i+1}\rangle\mid\] \[\text{H}\langle\text{interval}\rangle\langle\text{formula}_{i+1 }\rangle\mid\text{O}\langle\text{interval}\rangle\langle\text{formula}_{i +1}\rangle\] \[\langle\text{interval}\rangle ::=[\langle\text{num}\rangle,\langle\text{num}\rangle]\] \[\langle\text{atom}\rangle ::=\langle\text{attr}\rangle\langle\text{comp}\rangle\langle \text{num}\rangle\] \[\langle\text{attr}\rangle ::=a_{1}\mid a_{2}\mid\ldots\mid a_{|A|}\] \[\langle\text{comp}\rangle ::=\;<\;|\;>\] \[\langle\text{num}\rangle ::=\langle\text{digit}\rangle\langle\text{digit}\rangle\] \[\langle\text{digit}\rangle ::=0\mid 1\mid 2\mid 3\mid 4\mid 5\mid 6\mid 7\mid 8\mid 9\]  
When mapping a derivation tree into the corresponding STL formula, we apply the following adjustments concerning numerical parameters. To map a non-terminal interval symbol \(\langle\text{interval}\rangle\) into the corresponding time interval, we map the first \(\langle\text{num}\rangle\) into the corresponding integer in \(\{0,\ldots,99\}\) and set it to be the start of the interval.