where \(\top \triangleq \texttt {True}\) , \(p \in AP\)  and \(\bigcirc \)  (next), \(\textsf {U}\)  (until), \(\bot \triangleq \lnot \top \) . For brevity, we omit the derivations of other useful operators like \(\square \)  (always), \(\Diamond \)  (eventually), \(\Rightarrow \)  (implication).
The semantics of LTL is defined over the infinite words over \(2^{AP}\) . Intuitively, \(\sigma \in AP\)  is satisfied on a word \(w = w(1)w(2)w(3)\ldots \in (2^{AP})^{\omega }\)  if it holds at \(w(1)\) , i.e., if \(\sigma \in w(1)\) . Formula \(\bigcirc \, \varphi \)  holds true if \(\varphi \)  is satisfied on the word suffix that begins in the next position \(w(2)\) , whereas \(\varphi _1 \, \textsf {U}\, \varphi _2\)  states that \(\varphi _1\)  has to remain true until \(\varphi _2\)  becomes true. Finally, \(\Diamond \, \varphi \)  and \(\square \, \varphi \)  are true if \(\varphi \)  holds on \(w\)  eventually and always, respectively. We refer the readers to Chapter 5 of [1]} for the full definition of LTL syntax and semantics.
