| || |
Interval Temporal Logic (PITL)
Propositional Interval Temporal Logic (PITL) is a
- 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
- is an interval (sequence) of 2 states.
- is called ‘ chop ’ and denotes sequential composition of two
- is called ‘ chopstar’ and denotes (in)finite iteration of an interval.
The main semantic notion is interval which is a sequence of states.
- 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 .
- where denotes length of and is defined as
number of states minus 1