# Proving that a given formula in LTL is the smallest way to express it

I am looking for a way to prove that a given LTL formula is expressed with the fewest number of temporal operators possible.

I would like to do this to compare the expressive length with other temporal logic languages like MTL.

How can I prove that a given LTL formula is expressed most succinctly as possible? So as to say, this formula needs at least this many temporal operators.

For example, suppose I want to code that property p holds in every other state for the next 6 states starting from the current state, then I could specify this as, $$p \wedge XXp \wedge XXXXp \wedge XXXXXXp = p \wedge XX(p \wedge XX(p \wedge XXp))$$, where $$X$$ is the next operator, but how do I prove that this the smallest way to express this?

Your question is formally the same as this one: how many symbols $$X$$ are needed to write the polynomial $$XX + XXXX + XXXXXX = XX(1 + XX(1 + XX))$$? Well, you obtained $$6$$ as an upper bound. It is also a lower bound because any expression involving less than $$6$$ symbols $$X$$ would define a polynomial of degree $$< 6$$.