The key notion of ITL is an interval. An interval σ is considered to be a (in)ﬁnite sequence of states
σ_{0},σ_{1}…, where a state σ_{i} is a mapping from the set of variables Val to the set of values Val. The length
|σ|
of an interval σ_{0}…σ_{n} is equal to n, one less than the number of states in the interval (this has always
been a convention in ITL), i.e., a one state interval has length 0. The syntax of ITL is deﬁned in Table 1
where z is an integer value, a is a static integer variable (doesn’t change within an interval), A is a state integer variable (can change within an interval), v a static or state integer variable, g is a integer function symbol, q is a static Boolean variable (doesn’t change within an interval), Q is a state Boolean variable (can change within an interval), h is a predicate symbol.