ITL
© 1996-2015







10 Semantic Preliminaries

An interval σ is a (in)finite sequence of states

σ : σ0 σ1σ2...

Let  +
Σ  denote the set of all possible non-empty finite intervals. Let  ω
Σ denote the set of infinite intervals. [2mm] The length of an interval σ is denoted by |σ | and is the number of states minus 1.

Example 5

σ = σ0          |σ| = 0
σ = σ0σ1        |σ| = 1
σ = σ0σ1 ...σn  |σ| = n

_____________________________________________________________________

Static vs State Variables

  • Static variables don’t change their values within an interval.
  • State variables can change their values within an interval.
                 ⋃
V ar = Stat⋂eV ar   StaticV ar and
StateV ar   StaticV ar = ∅.

State variables are denoted by capital first symbols and static variables are denoted by small symbols.

Example 6 Let σ : σ σ
     0 1  be an interval where

σ0 (Q)  =   tt
σ0 (q)  =   ff
σ1 (Q)  =   ff
σ1 (q)  =   ff

Q is a state variable and q is a static variable.

_____________________________________________________________________

Let σ =  σ0σ1σ2 ... be an interval then

  • σ0 ...σk(where0 ≤ k ≤ |σ|) denotes a prefix interval of σ
  • σk ...σ|σ |(where0 ≤ k ≤ |σ|) denotes a suffix interval of σ
  • σ  ...σ (w here 0 ≤ k ≤ l ≤ |σ|)
 k     l denotes a sub interval of σ

Example 7 Let σ =  σ0σ1σ2σ3  be an interval then

σ0σ1     isa prefixintervalofσ
σ1σ2 σ3  isa suffi xintervalofσ
σ1σ2     isa sub intervalofσ

_____________________________________________________________________