ITL
© 1996-2015







11 Semantics of Propositional ITL

Let ⟦...⟧ be the “meaning” function from P IT L × (Σ+ ∪ Σ ω) to {tt,ff } and let σ be an interval (σ ∈ Σ+ ∪ Σ ω ) then

|------------------------------------------------|
|⟦true⟧σ      =^   tt                              |
|⟦q⟧σ        =^   σ0(q)and                       |
|                 for all0 < i ≤ |σ |,σi(q) = σ0(q)  |
|⟦Q ⟧σ       =^   σ0(Q )                         |
|⟦f ⟧σ      =^   not(⟦f ⟧σ )                      |
|⟦f1 ∧ f2⟧σ  =^   ⟦f1⟧σ and⟦f2⟧σ                  |
|⟦skip⟧σ = tt  iff   |σ| = 1                        |
-------------------------------------------------

The semantics of ‘chop’ is as follows ⟦f1 ; f2⟧σ = ttiff

|---------------------------------------------|
| (exists-k, s.t. ⟦f1⟧σ0...σk-=-ttand-⟦f2⟧σk...σ|σ| = tt)
| | | < —f  —  > | < —f  — >   |  |           |
| | σ      1    σ       2    σ    |           |
| | ∙0    ⋅⋅⋅    ∙k   ⋅⋅⋅     |∙σ| |           |
| ----------------------------------          |
-----------------------------------------------

Interval σ is a fusion of two intervals σ0 ...σk (satisfies f1  ) and σk ...σ|σ| (satisfies f2  ). State σk is shared by both.

|----------------------------|
| or(σ isinfinite and ⟦f1 ⟧σ = tt)|
||----------------|          |
||  | < — f1 — >  |          |
|| σ0             |          |
|| ∙     ⋅⋅⋅      |          |
|------------------          |
------------------------------

Interval σ is infinite and satisfies f
 1  , so f
 2  is irrelevant.

The semantics of ‘chopstar’ is as follows ⟦f*⟧ =  ttiff
    σ

ifσ isfinite then

|-------------------------------------------------------------|
|   (existl,...,l s.t. l = 0and l = |σ|and                      |
|    foral0l0 ≤ i <n n,l0≤ l  annd⟦f ⟧        = tt)               |
| |------------------i---i+1-------σli...σli+1------------------| |
| | | < —f — >  | ⋅⋅⋅ | < —f — >   |  ⋅⋅⋅  | <  —f — >  |   | |
| |σ0          σl1   σli         σli+1  σln-1          σ|σ| | |
| | ∙    ⋅⋅⋅    ∙ ⋅⋅⋅ ∙    ⋅⋅⋅     ∙  ⋅⋅⋅ ∙      ⋅⋅⋅    ∙   | |
| ----------------------------------------------------------- |
----------------------------------------------------------------

Finite interval σ is the fusion of a finite number of finite sub-intervals each satisfying f .

else

|--------------------------------------------------------|
|  (existl0,...,ln s.t. l0 = 0 and                          |
|   ⟦f ⟧σln...|σ| = ttand                                   |
|    forall0 ≤ i < n,li ≤ li+1 and ⟦f ⟧σl ...σl = tt)          |
||----------------------------------i---i+1------------|  |
||  | < —f — >  | ⋅⋅⋅ | < —f  — >   | ⋅⋅⋅ | < —f  — >  |  |
|| σ0          σl1  σli          σli+1   σln           |  |
|--∙----⋅⋅⋅-----∙-⋅⋅⋅-∙----⋅⋅⋅-----∙--⋅⋅⋅-∙-----⋅⋅⋅-----|  |
----------------------------------------------------------
                                                         |
Infinite interval σ is the fusion of a finite number of sub-intervals each satisfying f . Each sub-interval is finite except the last one which is infinite.

or

|--------------------------------------------|
|  (existan infinite num berofli s.t. l0 = 0 and      |
|    forall0 ≤ i,li ≤ li+1 and⟦f ⟧σ ...σ    = tt)  |
||-----------------------------li--li+1---|   |
||  | < —f — >  | ⋅⋅⋅ | < —f — >   | ⋅⋅⋅ |   |
|| σ0          σl1   σli          σli+1    |   |
||  ∙    ⋅⋅⋅    ∙ ⋅⋅⋅ ∙    ⋅⋅⋅     ∙ ⋅⋅⋅ |   |
|-----------------------------------------   |
---------------------------------------------|
Infinite interval σ is the fusion of an infinite number of finite sub-intervals each satisfying f .