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]

where

• skip is an interval (sequence) of 2 states.
• f₁ ; f₂ is called ‘f₁ chop f₂’ and denotes sequential composition of two intervals.
• f^∗ is called ‘f chopstar’ and denotes (in)finite iteration of an interval.

Derived formulae [Slide 7]

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,ff}.

Semantics of PITL [Slide 9]

• M⟦p⟧(σ) = tt iff σ₀(p) = tt
• M⟦¬f⟧(σ) = tt iff not (M⟦f⟧(σ) = tt)
• M⟦f₁ ∨ f₂⟧(σ) = tt iff M⟦f₁⟧(σ) = tt or M⟦f₂⟧(σ) = tt
• M⟦skip⟧(σ) = tt iff |σ| = 1 where |σ| denotes length of σ and is defined as number of states minus 1

• M⟦f1 ; f2⟧(σ) = tt iff

  ( exists k, s.t. M⟦f1⟧(σ0…σk) = tt and M⟦f2⟧(σk…σ|σ|) = tt)

  or (σ is infinite and M⟦f1⟧(σ) = tt)

Semantics of PITL [Slide 10]

• M⟦f∗⟧(σ) = 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 M⟦f⟧(σli…σli+1) = tt)

  else

  ( exists l0,…,ln s.t. l0 = 0 and

  M⟦f⟧(σln…σ|σ|) = tt and

  for all 0 ≤ i < n,li ≤ li+1 and M⟦f⟧(σli…σli+1) = tt)

  or

  ( exists an infinite number of li s.t. l0 = 0 and

  for all 0 ≤ i,li ≤ li+1 and M⟦f⟧(σli…σli+1) = tt)

Axiom/proof system for PITL [Slide 11]