ITL
© 1996-2016







2 Semantics

The informal semantics of the most interesting constructs are as follows:

  • C 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 ⟦...⟧e  be the “meaning” (semantic) function from Expressions  ×  (Σ+ ∪ Σ ω)  to Val  and let ⟦...⟧ be the “meaning” function from F ormulae ×  (Σ+ ∪ Σ ω)  to Bool  (set of Boolean values, {tt,ff} ) and let σ =  σ0σ1...  be an interval. We write        ′
σ ~v σ if the intervals σ  and  ′
σ are identical with the possible exception of their mappings for the variable v  . The formal semantics is listed in Table 2:


Table 2: Semantics of ITL
|------------------------------------------------------------------|
|⟦z⟧eσ                 =    ˆz                                       |
|⟦a⟧eσ                 =    σ0(a) and for all 0 < i ≤ |σ |,σi(a) = σ0(a )
|⟦A ⟧eσ                =    σ0(A)                                   |
|⟦g(e1,...,en)⟧e       =    ˆg(⟦e1⟧e,...,⟦en⟧e)                       |
|             σ            { σ (σA )       σ         if |σ | > 0      |
|⟦C A ⟧eσ               =        1                                   |
|                          { choose-any-from (V al)   otherwise       |
|⟦fin A⟧eσ              =      σ |σ|(A )                if σ is finite    |
|                            choose-any-from (V al)   otherwise       |
|⟦true⟧σ               =    tt                                      |
|⟦q⟧σ                 =    σ0(q) and for all 0 < i ≤ |σ |,σi(q) = σ0(q)
|⟦Q ⟧σ                =    σ0(Q)                                   |
|⟦h(e ,...,e )⟧ = tt  iff   ˆh(⟦e ⟧e,...,⟦e ⟧e)                       |
|    1      n σ                1σ       n σ                        |
|⟦f ⟧σ = tt          iff   not (⟦f⟧σ = tt)                          |
|⟦f1 ∧ f2⟧σ = tt       iff   (⟦f1⟧σ = tt) and (⟦f2⟧σ = tt)             |
|⟦skip ⟧σ = tt          iff   |σ | = 1                                 |
|⟦∀v  o f⟧ = tt        iff   (for all σ′ s.t. σ ~v σ′,⟦f ⟧σ′ = tt)       |
|⟦f1 ;f2⟧σ = tt        iff                                           |
|  (exists k, s.t. ⟦f1⟧σ0...σk = tt and ⟦f2⟧σk...σ = tt)                  |
|   or (σ is infinite and ⟦f ⟧ = tt)         |σ|                       |
|  *                     1 σ                                       |
|⟦f ⟧ = 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 ⟦f⟧σli...σli+1 = tt)                |
| else                                                              |
|  (exist l ,...,l s.t. l = 0 and                                    |
|         0     n     0                                            |
|    ⟦f ⟧σln...|σ| = tt and                                            |
|    for all 0 ≤ i < n,li ≤ li+1 and ⟦f⟧σli...σli+1 = tt)                |
|   or                                                             |
|  (exist an infinite number of li s.t. l0 = 0 and                    |
|    for all 0 ≤ i,li ≤ li+1 and ⟦f⟧σl...σl = tt)                      |
---------------------------------i---i+1-----------------------------