V.9 Summary

Summary [Slide 168]

• A first order ITL formula contains predicates, propositional variables, Boolean operators, temporal operators and quantifiers.
• The semantics (meaning) of a first order ITL formula is defined with respect to an interval (non-empty sequence of states).
• One can define the satisfiability and validity of an ITL formula.