<p>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.</p>
<p>Probably the most recent paper to read is by Lauri Hella and Miikka Vilander. Its free-access version is available on arxiv <a href="https://arxiv.org/pdf/1912.08715.pdf" rel="nofollow noreferrer">here</a>.</p>

CC BY-SA 4.0
2021-06-17T07:01:28.897Z
2021-06-17T07:01:28.897Z
Bartosz Bednarczyk
<p>Your question is formally the same as this one: how many symbols <span class="math-container">$X$</span> are needed to write the polynomial <span class="math-container">$XX + XXXX + XXXXXX = XX(1 + XX(1 + XX))$</span>?
Well, you obtained <span class="math-container">$6$</span> as an upper bound. It is also a lower bound because any expression involving less than <span class="math-container">$6$</span> symbols <span class="math-container">$X$</span> would define a polynomial of degree <span class="math-container">$&lt; 6$</span>.</p>
<p>For the general case, I would not be surprised if it turns out to be a NP-complete problem.</p>

CC BY-SA 4.0
2021-06-17T05:15:26.587Z
2021-06-17T05:15:26.587Z
J.-E. Pin
<p>I am looking for a way to prove that a given LTL formula is expressed with the fewest number of temporal operators possible.</p>
<p>I would like to do this to compare the expressive length with other temporal logic languages like MTL.</p>
<p>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.</p>
<p>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, <span class="math-container">$p \wedge XXp \wedge XXXXp \wedge XXXXXXp = p \wedge XX(p \wedge XX(p \wedge XXp))$</span>, where <span class="math-container">$X$</span> is the next operator, but how do I prove that this the smallest way to express this?</p>

<proofs><linear-temporal-logic>
Proving that a given formula in LTL is the smallest way to express it
Gokul
# Proving that a given formula in LTL is the smallest way to express it

(Asked by: username_0 on 2021-06-17)

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?

**Tags:** proofs, linear-temporal-logic

---

## 2 answers

### Answer by username_1 on 2021-06-17. Score: 2 | Accepted answer

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](https://arxiv.org/pdf/1912.08715.pdf).


---

### Answer by username_2 on 2021-06-17. Score: 1

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.


---

