#### 1.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 the interval is non-empty then the value of A in the next state of that interval else an arbitrary value.
• ﬁn A: the value of A in the last state of the interval.
• 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 interval and f2 over the suﬃx interval.
• f holds if the interval is decomposable into a ﬁnite number of intervals such that for each of them f holds.

Let Σ+ denote the set of all ﬁ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 2:

Table 2: Semantics of ﬁ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)
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)
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)
Mf(σ) = tt
iﬀ
(exist l0,,ln s.t. l0 = 0 and ln = |σ| and
for all 0 i < n,li < li+1 and Mf(σliσli+1) = tt)

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