ITL
© 1996-2015







12 Derived Propositional ITL formulae

We will now introduce some derived temporal formulae.

C f     ^=   skip ;f        next
c f     ^=    Cf         weaknext
m ore    ^=   C true         non-emptyinterval
em pty   ^=   m ore        em pty interval
inf      ^=   true ;false     infiniteinterval
finite    ^=   inf          finiteinterval
  f     ^=   finite;f        som etimes
! f     ^=      f        always
i f     ^=   f ;true        som einitialsubinterval
I f     ^=   (i f )      allinitialsubintervals
a f     ^=   finite;f ;true  som esubinterval
A f     ^=   (a f )      allsubintervals

  • Next, f holds in the next state of the interval:

    |------------------------------------------|
| Cf-=^-skip;f---------------------------|  |
| ⟦C f⟧σ = ttiff |σ | > 0 and(⟦f⟧σ1...σ|σ| = tt)  |
| ---------------------------------------  |
--------------------------------------------

  • Weak Next, interval has only one state or f holds in the next state of the interval:

    |-----------------------------------------|
| cf-=^-C-f--------------------------|  |
| ⟦c f⟧σ = ttiff |σ | = 0 or(⟦f ⟧σ1...σ|σ| = tt)  |
-------------------------------------------

  • More, interval with at least two states:

    |-------------------------|
| more ^=   true            |
| |------C-------------|  |
| ⟦m-ore⟧σ-=-ttiff-|σ| >-0-  |
---------------------------

  • Empty, interval with only one state:

    |-------------------------|
| empty=^-m-ore---------| |
| ⟦em-pty⟧σ-=-ttiff-|σ-| =-0- |
----------------------------

  • Infinite, interval with an infinite number of states:

    |-------------------------|
| inf=^-true;false---------| |
| ⟦in-f⟧σ-=-ttiff-σ-isinfinite-- |
----------------------------

  • Finite, interval with a finite number of states:

    |--------------------------|
| finite=^-inf------------|  |
| ⟦finite⟧σ = ttiff σ isfinite |  |
----------------------------

  • Sometimes, there exist a suffix interval that satisfies f :

    |----------------------------------------------------|
| |-f=^-finite;f-------------------------------------| |
| ⟦  f⟧σ = ttiff (existsa 0 ≤ k ≤ |σ|,s.t.⟦f⟧σk...σ   = tt) | |
| -----------------------------------------|σ|------ |
-------------------------------------------------------

  • Always, all suffix intervals satisfy f :

    |----------------------------------------------------|
| !f-=^---f-------------------------------------|  |
| ⟦! f⟧σ = ttiff (forall0 ≤ k ≤ |σ |, s.t.⟦f ⟧σk...σ|σ| = tt)|  |
| -------------------------------------------------  |
------------------------------------------------------

  • Diamond-i, there exists a prefix interval that satisfies f :

    |----------------------------------------------------|
| i-f=^-f-;true------------------------------------|  |
| ⟦i f⟧σ = ttiff (existsa 0 ≤ k ≤ |σ|, s.t.⟦f ⟧σ ...σ = tt)|  |
| ---------------------------------------0--k------  |
------------------------------------------------------

  • Box-i, all prefix intervals satisfy f :

    |-------------------------------------------------|
| If =^  if                                     |
| |---------------------------------------------| |
| ⟦I-f⟧-=-ttiff-(forall0 ≤-k ≤-|σ-|,-s.t.⟦f⟧σ0...σk =-tt)- |
----------------------------------------------------

  • Diamond-a, there exists a sub-interval that satisfies f :

    |---------------------------------------------------|
| a f=^ finite;f ;true                                 |
| |----------------------------------------------|  |
| ⟦a-f⟧-=-ttiff-(exist0 ≤-k ≤-l ≤-|σ|s.t.⟦f⟧σk...σl-=-tt)  |
-----------------------------------------------------

  • Box-a, all sub-intervals satisfy f :

    |----------------------------------------------------|
| Af-=^--af-------------------------------------|  |
| ⟦A-f⟧-=-ttiff-(forall0 ≤-k ≤-l ≤-|σ|s.t.⟦f⟧σk...σl-=-tt)  |
------------------------------------------------------

  • Following are derived temporal formulae that are “programming constructs”:
    iff0 then f1 else f2=^ (f0 ∧ f1) ∨ (f0 ∧ f2) ifthenelse
iff0 then f1     =^  iff0 the n f1 else em pty  ifthen
haltf            =^  !(em pty ≡ f )          haltw hen
keep f           =^  A(skip ⊃ f)            allunitsub-intervals
w hile f0 do f1    =^  (f0 ∧ f1)* ∧ finf0     while loop
repeatf0untilf1   =^  f0 ; (w hilef1 do f0)   repeatloop