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?