Temporal Logic:
Linear Temporal Logic (LTL):
(Next), in the next state,
(Always), all states in the behaviour,
(Sometimes), exist a state in the behaviour
Interval Temporal Logic (ITL):
skip, behaviour of two states,
; (Chop), fusion of two behaviours,
^{∗} (chopstar), fusion of a ﬁnite number of behaviours
Propositional Interval Temporal Logic (PITL):
ITL with only propositional variables, i.e., Boolean values.
Veriﬁcation tools for Propositional Interval Temporal (PITL):