ITL
© 1996-2018







III.3 Semantic Preliminaries

Interval and Length [Slide 93]

An interval σ is a finite sequence of states

σ : σ0σ1σ2

Let Σ+ denote the set of all finite intervals with at least 1 state. The length of an interval σ is denoted by |σ| and is the number of states minus 1.

Example 26.  

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

Static and State Variables [Slide 94]

  • Static variables don’t change their values within an interval.
  • State variables can change their values within an interval.

Var = StateVar StaticVar and
StateVar StaticVar = .

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

Example 27.  

Let σ : σ0σ1 be an interval where

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

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

Prefix, Suffix and Sub Interval [Slide 95]

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 σ

Example 28.  

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

σ0σ1
is a prefix interval of σ
σ1σ2σ3
is a suffix interval of σ
σ1σ2
is a sub interval of σ







2018-03-10
Contact | Home | ITL home | Course | Proofs | Algebra | FL