### 3 Propositional Interval Temporal Logic (PITL)

#### PITL [Slide 5]

Propositional Interval Temporal Logic (PITL) is a

• discrete,
• linear temporal logic
• for both ﬁnite and inﬁnite 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)ﬁnite 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 inﬁnite interval ﬁnite ≜ ¬inf ﬁnite interval fmore ≜ more ∧ﬁnite ﬁnite with ≥ 2 states f ≜ ﬁnite ; f sometimes f ≜ ¬¬f always f ≜ f ; true some initial subinterval f ≜ ¬( ¬f) all initial subintervals f ≜ ﬁnite ; 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 ﬁnite sequences of states.
• Σω denote the set of inﬁnite sequences of states.
• σ denote an interval, σ Σ+ Σω.
• Let M() be the “meaning” (semantic) function from Σ+ Σω to {tt,}.

#### Semantics of PITL [Slide 9]

• Mp(σ) = tt iﬀ σ0(p) = tt
• M¬f(σ) = tt iﬀ not (Mf(σ) = tt)
• Mf1 f2(σ) = tt iﬀ Mf1(σ) = tt or Mf2(σ) = tt
• Mskip(σ) = tt iﬀ |σ| = 1 where |σ| denotes length of σ and is deﬁned as number of states minus 1
•  M⟦f1 ; f2⟧(σ) = tt iﬀ ( exists k, s.t. M⟦f1⟧(σ0…σk) = tt and M⟦f2⟧(σk…σ|σ|) = tt) or (σ is inﬁnite and M⟦f1⟧(σ) = tt)

#### Semantics of PITL [Slide 10]

•  M⟦f∗⟧(σ) = tt iﬀ if σ is ﬁnite 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 inﬁnite 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]

 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-26 Contact | Home | ITL home | Course | Proofs | Algebra | FL