ITL
© 1996-2015







3 Propositional Interval Temporal Logic (PITL)

Propositional Interval Temporal Logic (PITL) is a

  • discrete,
  • linear temporal logic
  • for both finite and infinite time which includes
  • a basic construct for sequential composition and
  • an analog of Kleene star and Omega star
f ::=  p |f |f1 ∨ f2|skip|f1 ; f2|f*

where

  • skip  is an interval (sequence) of 2 states.
  • f1 ;f2  is called ‘f1  chop f2  ’ and denotes sequential composition of two intervals.
  • f* is called ‘f chopstar’ and denotes (in)finite iteration of an interval.
C f     ^=   skip ;f        next
c f     ^=    Cf         weaknext
m ore    ^=   C true         intervalwith ≥ 2states
em pty   ^=   m ore        one state interval
inf      ^=   true ;false     infiniteinterval
finite    ^=   inf          finiteinterval
fm ore   ^=   mo re ∧ finite   finitewith ≥ 2states
  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
etc.

The main semantic notion is interval which is a sequence of states.

Let

  • Σ denotes the set of states.
  • Σ+  denote the set of non-empty finite sequences of states.
  •   ω
Σ denote the set of infinite sequences of states.
  • σ denote an interval, σ ∈ Σ+  ∪ Σω .
  • Let ⟦...⟧ be the “meaning” (semantic) function from  +     ω
Σ  ∪ Σ to {tt,ff} .
  • ⟦p⟧σ = ttiff σ0(p) = tt
  • ⟦f ⟧σ = ttiff not(⟦f⟧σ = tt)
  • ⟦f1 ∨ f2 ⟧σ = ttiff ⟦f1⟧σ = ttor⟦f2⟧σ = tt
  • ⟦skip⟧σ = ttiff |σ | = 1 where |σ| denotes length of σ and is defined as number of states minus 1
  • ⟦f1 ;f2⟧σ = ttiff
(exists k, s.t.⟦f1⟧σ0...σk = ttand ⟦f2⟧σk...σ|σ| = tt)
or (σ isinfiniteand⟦f1⟧σ = tt)
  • ⟦f*⟧σ = ttiff
ifσ isfinitethen
  (existl0,...,ln s.t.l0 = 0 and ln = |σ |and
   forall0 ≤ i < n,li ≤ li+1 and ⟦f⟧σli...σli+1 = tt)
else
  (existl0,...,ln s.t.l0 = 0 and
   ⟦f⟧σln...σ|σ| = ttand
    forall0 ≤ i < n, li ≤ li+1 and⟦f⟧σl...σl  = tt)
   or                              i  i+1
  (existaninfinitenum berof li s.t.l0 = 0and
    forall0 ≤ i,li ≤ li+1 and⟦f⟧σ ...σ    = tt)
                              li   li+1
PropAx        A llaxiomsforpropositionallogic
C hopA ssoc     ⊢ (f0 ;f1);f2 ≡ f0 ;(f1 ;f2)
O rC hopIm p    ⊢ (f0 ∨ f1);f2 ⊃ (f0 ;f2) ∨ (f1 ;f2)
C hopO rIm p    ⊢ f0 ;(f1 ∨ f2) ⊃ (f0 ;f1) ∨ (f0 ;f2)
E mptyC hop    ⊢ em pty;f1 ≡ f1
C hopE mpty    ⊢ f1 ;em pty ≡ f1
B iBoxC hop    ⊢ I (f0 ⊃ f1) ∧ ! (f2 ⊃ f3) ⊃ (f0 ;f2) ⊃ (f1 ;f3)
StateImpB i    ⊢ p ⊃  I p
N extImpW Next ⊢ C f0 ⊃  C f0
SkipAnd       ⊢ (skip ∧ f0) ;true ⊃  ((skip ∧ f0 );true )
B oxInduct     ⊢ f0 ∧ ! (f0 ⊃  C f0) ⊃  !f0
C hopS tarEqv   ⊢ f *0 ≡ (e mpty ∨ ((f0 ∧ more); f*0))
C hopS tarInduct ⊢ (inf ∧ f0 ∧ !(f0 ⊃ (f1 ∧ fm ore) ;f0)) ⊃ f*1
M P           ⊢ f0 ⊃ f1 and ⊢ f0 implies ⊢ f1
B oxGen       ⊢ f0 im plies ⊢ !f0
B iG en         ⊢ f0 im plies ⊢ If0