### 1 Syntax

The key notion of ITL is an interval. An interval σ is considered to be a (in)ﬁnite sequence of states σ01, 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.

Table 1: Syntax of ITL
 Expressions e ::= z|a|A|g(e1,…,en)|A| ﬁn A Formulae f ::= true|q|Q| h(e1,…,en)|¬f|f1 ∧ f2|∀v f|skip|f1 ; f2|f∗

 2018-03-10 Contact | Home | ITL home | Course | Proofs | Algebra | FL