The Linear Temporal Logic (short LTL) is a mathematical logic that is able to talk about the future of paths. LTL is build up from proposition variables p 1 , p 2 {\displaystyle p_{1},p_{2}} , the usual logic connectives ¬ , ∨ , ∧ , → {\displaystyle \neg ,\lor ,\land ,\rightarrow }
