#### 2.2 Semantics

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.
• ﬁn A: 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).
• f1 ; f2 holds if the interval can be decomposed (“chopped”) into a preﬁx and suﬃx interval, such that f1 holds over the preﬁx and f2 over the suﬃx, or if the interval is inﬁnite and f1 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
Ez(σ)
=
z
Ea(σ)
=
σ0(a) and for all 0 < i |σ|i(a) = σ0(a)
EA(σ)
=
σ0(A)
Eig(ie1,,ien)(σ)
=
ig(Eie1(σ),, Eien(σ))
EA(σ)
=
 σ1(A) if |σ| > 0 choose-any-from(ℤ) otherwise
Eﬁn A(σ)
=
 σ|σ|(A) if σ is ﬁnite choose-any-from(ℤ) otherwise
Eb(σ)
=
b
Eq(σ)
=
σ0(q) and for all 0 < i |σ|i(q) = σ0(q)
EQ(σ)
=
σ0(Q)
Ebg(be1,,ben)(σ)
=
bg(Ebe1(σ),, Eben(σ))
EQ(σ)
=
 σ1(Q) if |σ| > 0 choose-any-from(Bool) otherwise
Eﬁn Q(σ)
=
 σ|σ|(Q) if σ is ﬁnite choose-any-from(Bool) otherwise
Mtrue(σ)
=
tt
Mh(e1,,en)(σ) = tt
iﬀ
h(Ee1(σ),, Een(σ))
M¬f(σ) = tt
iﬀ
not (Mf(σ) = tt)
Mf1 f2(σ) = tt
iﬀ
(Mf1(σ) = tt) and (Mf2(σ) = tt)
Mskip(σ) = tt
iﬀ
|σ| = 1
Mv f(σ) = tt
iﬀ
(for all σ s.t. σ vσ, Mf(σ) = tt)
Mf1 ; f2(σ) = tt
iﬀ
(exists k, s.t. Mf1(σ0σk) = tt and Mf2(σkσ|σ|) = tt)
or (σ is inﬁnite and Mf1(σ) = tt)
Mf(σ) = tt
iﬀ
if σ is ﬁnite then
(exist l0,,ln s.t. l0 = 0 and ln = |σ| and
for all 0 i < n,li < li+1 and Mf(σliσli+1) = tt)
else
(exist l0,,ln s.t. l0 = 0 and
Mf(σlnσ|σ|) = tt and
for all 0 i < n,li < li+1 and Mf(σliσli+1) = tt)
or
(exist an inﬁnite number of li s.t. l0 = 0 and
for all 0 i,li < li+1 and Mf(σliσli+1) = tt)

 2019-03-16 Contact | Home | ITL home | Course | Proofs | Algebra | FL