  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
where
 is an interval (sequence) of 2 states.
 is called ‘ chop ’ and denotes sequential composition of two
intervals.
 is called ‘ chopstar’ and denotes (in)finite iteration of an interval.
The main semantic notion is interval which is a sequence of states.
Let
 denotes the set of states.
 denote the set of nonempty finite sequences of states.
 denote the set of infinite sequences of states.
 denote an interval, .
 Let be the “meaning” (semantic) function from to .



 where denotes length of and is defined as
number of states minus 1
  