© 1996-2019







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 prefix interval of σ
  • σkσ|σ|(where 0 k |σ|) denotes a suffix 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.
  • fin A: if interval is finite 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 prefix and suffix interval, such that f1 holds over the prefix and f2 over the suffix, or if the interval is infinite and f1 holds for that interval.
  • f holds if the interval is decomposable into a finite number of intervals such that for each of them f holds, or the interval is infinite and can be decomposed into an infinite number of finite intervals for which f holds.

Let Σ+ denote the set of all finite intervals and Σω denotes the set of all infinite 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 finite and infinite ITL
Ez(σ)
=
z
EA(σ)
=
σ0(A)
Eig(ie1,,ien)(σ)
=
ig(Eie1(σ),, Eien(σ))
EA(σ)
=
σ1(A)
if |σ| > 0
choose-any-from()
otherwise
Efin A(σ)
=
σ|σ|(A)
if σ is finite
choose-any-from()
otherwise
Eb(σ)
=
b
EQ(σ)
=
σ0(Q)
Ebg(be1,,ben)(σ)
=
bg(Ebe1(σ),, Eben(σ))
EQ(σ)
=
σ1(Q)
if |σ| > 0
choose-any-from(Bool)
otherwise
Efin Q(σ)
=
σ|σ|(Q)
if σ is finite
choose-any-from(Bool)
otherwise
Mtrue(σ)
=
tt
Mh(e1,,en)(σ) = tt
iff
h(Ee1(σ),, Een(σ))
M¬f(σ) = tt
iff
not (Mf(σ) = tt)
Mf1 f2(σ) = tt
iff
(Mf 1(σ) = tt) and (Mf2(σ) = tt)
Mskip(σ) = tt
iff
|σ| = 1
MV f(σ) = tt
iff
(for all σ s.t. σ V σ, Mf(σ) = tt)
Mf1 ; f2(σ) = tt
iff
(exists k, s.t. Mf1(σ0σk) = tt and Mf2(σkσ|σ|) = tt)
or (σ is infinite and Mf1(σ) = tt)
Mf(σ) = tt
iff
if σ is finite 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 infinite number of li s.t. l0 = 0 and
  for all 0 i,li < li+1 and Mf(σliσli+1) = tt)







2019-07-23
Contact | Home | ITL home | Course | Proofs | Algebra | FL