© 1996-2019







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 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 the interval is non-empty then the value of A in the next state of that interval else an arbitrary value.
  • fin 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 prefix and suffix interval, such that f1 holds over the prefix interval and f2 over the suffix interval.
  • f holds if the interval is decomposable into a finite number of intervals such that for each of them f holds.

Let Σ+ denote the set of all finite 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 finite ITL
Ez(σ)
=
z
EA(σ)
=
σ0(A)
Eig(ie1,,ien)(σ)
=
ig(Eie1(σ),, Eien(σ))
EA(σ)
=
σ1(A)
if |σ| > 0
choose-any-from()
otherwise
Efin A(σ)
=
σ|σ|(A)
Eb(σ)
=
b
EQ(σ)
=
σ0(Q)
Ebg(be1,,ben)(σ)
=
bg(Ebe1(σ),, Eben(σ))
EQ(σ)
=
σ1(Q)
if |σ| > 0
choose-any-from(Bool)
otherwise
Efin Q(σ)
=
σ|σ|(Q)
Mtrue(σ)
=
tt
Mh(e1,,en)(σ) = tt
iff
h(Ee1(σ),, Een(σ))
M¬f(σ) = tt
iff
not (Mf(σ) = tt)
Mf1 f2(σ) = tt
iff
(Mf1(σ) = 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)
Mf(σ) = tt
iff
(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-07-23
Contact | Home | ITL home | Course | Proofs | Algebra | FL