Each state σ_{i} is the union of the mapping from the set of integer variables IntVar to the set of integer values ℤ and the mapping from propositional variables PropVar to set of Boolean values {tt, ﬀ}.
Each interval has at least one state. 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. Let σ = σ_{0}σ_{1}σ_{2}… be an interval then
The informal semantics of the most interesting constructs are as follows:
Let Σ^{+} denote the set of all ﬁnite intervals and Σ^{ω} denotes the set of all inﬁnite intervals.
Let Expressions denote the set of (integer or Boolean) expressions.
Let Val denote the set of integer or Boolean values (ℤ ∪ Bool).
Let E⟦…⟧( ) denote the meaning function from Expressions × (Σ^{+} ∪ Σ^{ω}) to Val.
Let Formulae denote the set of ITL formulae.
Let M⟦…⟧( ) denote the meaning function from Formulae × (Σ^{+} ∪ Σ^{ω}) to Bool (set of Boolean
values, {tt, ﬀ}).
Let σ = σ_{0}σ_{1}… denote an interval.
We write σ ∼_{V } σ′ if the intervals σ and σ′ are identical with the possible exception of their mappings for
the variable V .
Let chooseanyfrom(Val) denote the choice function that selects an arbitrary value from Val.
The formal semantics is listed in Table 10:
E⟦z⟧(σ) 
= 
z 

E⟦A⟧(σ) 
= 
σ_{0}(A) 

E⟦ig(ie_{1},…,ie_{n})⟧(σ) 
= 
ig(E⟦ie_{1}⟧(σ),…, E⟦ie_{n}⟧(σ)) 

E⟦ A⟧(σ) 
= 


E⟦ﬁn A⟧(σ) 
= 


E⟦b⟧(σ) 
= 
b 

E⟦Q⟧(σ) 
= 
σ_{0}(Q) 

E⟦bg(be_{1},…,be_{n})⟧(σ) 
= 
bg(E⟦be_{1}⟧(σ),…, E⟦be_{n}⟧(σ)) 

E⟦ Q⟧(σ) 
= 


E⟦ﬁn Q⟧(σ) 
= 


M⟦true⟧(σ) 
= 
tt 

M⟦h(e_{1},…,e_{n})⟧(σ) = tt 
iﬀ 
h(E⟦e_{1}⟧(σ),…, E⟦e_{n}⟧(σ)) 

M⟦¬f⟧(σ) = tt  iﬀ  not (M⟦f⟧(σ) = tt) 

M⟦f_{1} ∧ f_{2}⟧(σ) = tt  iﬀ  (M⟦f_{
1}⟧(σ) = tt) and (M⟦f_{2}⟧(σ) = tt) 

M⟦skip⟧(σ) = tt 
iﬀ 
σ = 1 

M⟦∀V f⟧(σ) = tt 
iﬀ 
(for all σ′ s.t. σ ∼_{V } σ′, M⟦f⟧(σ′) = tt) 

M⟦f_{1} ; f_{2}⟧(σ) = tt 
iﬀ 

(exists k, s.t. M⟦f_{1}⟧(σ_{0}…σ_{k}) = tt and M⟦f_{2}⟧(σ_{k}…σ_{σ}) = tt)
 
or (σ is inﬁnite and M⟦f_{1}⟧(σ) = tt)
 
M⟦f^{∗}⟧(σ) = tt 
iﬀ 

if σ is ﬁnite then
 
(exist l_{0},…,l_{n} s.t. l_{0} = 0 and l_{n} = σ and
 
for all 0 ≤ i < n,l_{i} < l_{i+1} and M⟦f⟧(σ_{li}…σ_{li+1}) = tt)
 
else
 
(exist l_{0},…,l_{n} s.t. l_{0} = 0 and
 
M⟦f⟧(σ_{ln}…σ_{σ}) = tt and
 
for all 0 ≤ i < n,l_{i} < l_{i+1} and M⟦f⟧(σ_{li}…σ_{li+1}) = tt)
 
or
 
(exist an inﬁnite number of l_{i} s.t. l_{0} = 0 and
 
for all 0 ≤ i,l_{i} < l_{i+1} and M⟦f⟧(σ_{li}…σ_{li+1}) = tt)
 