
 III.6 Summary
Summary [Slide 100]
 An ITL formula contains propositional variables, Boolean
operators and temporal operators.
 The semantics (meaning) of an ITL formula is deﬁned with
respect to an interval (nonempty sequence of states).
 One can deﬁne the satisﬁability and validity of an ITL formula.
  