Temporal logic can be more expressive

We start by proving that some properties of sequences are not expressible in Temporal Logic though they are expressible using for instance regular expressions. Then, we show how Temporal Logic can be extended to express any such property definable by a right-linear grammar and hence a regular expression, Finally, we give a decision procedure and complete axiomatization for the extended Temporal Logic.