ITL
© 1996-2018







3 Propositional Interval Temporal Logic (PITL)

PITL [Slide 5]

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

Syntax of PITL [Slide 6]

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.

Derived formulae [Slide 7]

f
skip ; f

next

f
¬¬f

weak next

more
true

interval with 2 states

empty
¬more

one state interval

inf
true ; false

infinite interval

finite
¬inf

finite interval

fmore
more finite

finite with 2 states

f
finite ; f

sometimes

f
¬¬f

always

f
f ; true

some initial subinterval

f
¬( ¬f)

all initial subintervals

f
finite ; f ; true

some subinterval

f
¬( ¬f)

all subintervals

etc.

Semantics of PITL [Slide 8]

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 M() be the “meaning” (semantic) function from Σ+ Σω to {tt,}.

Semantics of PITL [Slide 9]

  • Mp(σ) = tt iff σ0(p) = tt
  • M¬f(σ) = tt iff not (Mf(σ) = tt)
  • Mf1 f2(σ) = tt iff Mf1(σ) = tt or Mf2(σ) = tt
  • Mskip(σ) = tt iff |σ| = 1 where |σ| denotes length of σ and is defined as number of states minus 1
  • Mf1 ; f2(σ) = tt iff
    ( exists k, s.t. Mf1(σ0σk) = tt and Mf2(σkσ|σ|) = tt)
    or (σ is infinite and Mf1(σ) = tt)

Semantics of PITL [Slide 10]

  • Mf(σ) = tt iff
    if σ is finite then
    ( exists l0,,ln s.t. l0 = 0 and ln = |σ| and
      for all 0 i < n,li li+1 and Mf(σliσli+1) = tt)
    else
    ( exists l0,,ln s.t. l0 = 0 and
      Mf(σlnσ|σ|) = tt and
      for all 0 i < n,li li+1 and Mf(σliσli+1) = tt)
    or
    ( exists an infinite number of li s.t. l0 = 0 and
      for all 0 i,li li+1 and Mf(σliσli+1) = tt)

Axiom/proof system for PITL [Slide 11]

PropAx
All axioms for propositional logic
ChopAssoc
(f0 ; f1) ; f2 f0 ; (f1 ; f2)
OrChopImp
(f0 f1) ; f2 (f0 ; f2) (f1 ; f2)
ChopOrImp
f0 ; (f1 f2) (f0 ; f1) (f0 ; f2)
EmptyChop
empty ; f1 f1
ChopEmpty
f1 ; empty f1
BiBoxChop
(f0 f1) (f2 f3) (f0 ; f2) (f1 ; f3)
StateImpBi
p p
NextImpWNext
f0 ¬¬f0
SkipAnd
(skip f0) ; true ¬((skip ¬f0) ; true)
BoxInduct
f0 (f0 ¬¬f0) f0
ChopStarEqv
f0 (empty ((f0 more) ; f0))
ChopStarInduct
(inf f0 (f0 (f1 fmore) ; f0)) f1
MP
f0 f1 and f0 implies f1
BoxGen
f0 implies f0
BiGen
f0 implies f0







2018-02-25
Contact | Home | ITL home | Course | Proofs | Algebra | FL