Atomic propositions are Boolean variables that can be either true or false. The ingredients of an LTL formula are a set of atomic propositions \(AP\)  and several boolean and temporal operators, with the following syntax [1]}:
\(\varphi ::=\top \;|\; p \;|\; \varphi _1 \wedge \varphi _2 \;|\; \lnot \varphi \;|\; \bigcirc \varphi \;|\; \varphi _1\, \textsf {U}\, \varphi _2,\) 
