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

σ_{0}…σ_{k}(where 0 ≤ k ≤|σ|) denotes a preﬁx interval of σ

σ_{k}…σ_{|σ|}(where 0 ≤ k ≤|σ|) denotes a suﬃx interval of σ

σ_{k}…σ_{l}(where 0 ≤ k ≤ l ≤|σ|) denotes a sub interval of σ

The informal semantics of the most interesting constructs are as follows:

A: if interval is non-empty then the value of A in the next state of that interval else an
arbitrary value.

ﬁnA: if interval is ﬁnite then the value of A in the last state of that interval else an arbitrary
value.

skip unit interval (length 1).

f_{1};f_{2} holds if the interval can be decomposed (“chopped”) into a preﬁx and suﬃx interval,
such that f_{1} holds over the preﬁx and f_{2} over the suﬃx, or if the interval is inﬁnite and f_{1}
holds for that interval.

f^{∗} holds if the interval is decomposable into a ﬁnite number of intervals such that for each
of them f holds, or the interval is inﬁnite and can be decomposed into an inﬁnite number of
ﬁnite intervals for which f holds.

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 choose-any-from(Val) denote the choice function that selects an arbitrary value from Val.
The formal semantics is listed in Table 10:

Table 10:Semantics of ﬁnite and inﬁnite ITL

E⟦z⟧(σ)

=

z

E⟦A⟧(σ)

=

σ_{0}(A)

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

=

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

E⟦A⟧(σ)

=

σ_{1}(A)

if |σ|> 0

choose-any-from(ℤ)

otherwise

E⟦ﬁnA⟧(σ)

=

σ_{|σ|}(A)

if σ is ﬁnite

choose-any-from(ℤ)

otherwise

E⟦b⟧(σ)

=

b

E⟦Q⟧(σ)

=

σ_{0}(Q)

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

=

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

E⟦Q⟧(σ)

=

σ_{1}(Q)

if |σ|> 0

choose-any-from(Bool)

otherwise

E⟦ﬁnQ⟧(σ)

=

σ_{|σ|}(Q)

if σ is ﬁnite

choose-any-from(Bool)

otherwise

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⟦∀Vf⟧(σ) = 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)