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?


I'm not sure whether it would work in your case, but in order to show succinctness results in modal/temporal logic (e.g. the fact the two-variable logic over words in exponentially more succinct than unary temporal logic) one can employ formula size games or Adler-Immerman games.

Probably the most recent paper to read is by Lauri Hella and Miikka Vilander. Its free-access version is available on arxiv here.


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$.

For the general case, I would not be surprised if it turns out to be a NP-complete problem.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.