<p>Decidability of Craig Interpolant Existence for LTL over finite words follows from:</p>
<p>[1] K. Henkell. 1988. Pointlike sets: The finest aperiodic cover of a finite semigroup. Journal of Pure and Applied Algebra
55, 1-2 (1988), 85–126.</p>
<p>[2] K. Henkell, J. Rhodes, and B. Steinberg. 2010. Aperiodic pointlikes and beyond. International Journal of Algebra and
Computation 20, 2 (2010), 287–305,</p>
<p>while the case of omega-word is treated in:</p>
<p>[3]  Thomas Place and Marc Zeitoun. 2016. Separating regular languages with first-order logic. Logical Methods in Computer Science 12, 1:5 (2016), 1–30</p>
<p>These results are formulated in terms of the separability problem but CIP Existence and separability are known to be equivalent.</p>
<p>You may also be interested in the following paper:</p>
<p>[4] Jean Christoph Jung, Jedrzej Kolodziejski:
Modal Separability of Fixpoint Formulae. Description Logics 2024</p>

CC BY-SA 4.0
2024-09-17T10:59:58.250Z
Thank you! That's exactly what I was looking for!
Nicola Gigante
CC BY-SA 4.0
2024-09-16T13:16:23.733Z
2024-09-16T13:22:55.710Z
2024-09-16T13:22:55.710Z
Bartosz Bednarczyk
<p>It is known that Linear Temporal Logic (LTL) does <em>not</em> support Craig's theorem, so there are formulas <span class="math-container">$\phi$</span> and <span class="math-container">$\psi$</span> where <span class="math-container">$\phi\to\psi$</span> holds but an interpolant does not exist.</p>
<p>In principle, there may be fragments of LTL supporting interpolation, a trivial special case being the propositional fragment where the original Craig's theorem applies.</p>
<p>However, I've found some literature about the topic and it seems there are not useful proper fragments of LTL supporting interpolation apart from the one with only the <em>tomorrow</em> operator which is just syntactic-sugar on top of propositional logic and is not really interesting.</p>
<p>So I cannot have guarantees that an interpolant exists between <span class="math-container">$\phi$</span> and <span class="math-container">$\psi$</span>, however is there an algorithmic way to compute an interpolant <em>if</em> it exists?</p>
<p>I'm interested both in LTL on infinite and finite words, if it makes any difference (btw, I don't know if everything above holds for finite words as well: is it true that LTL on finite words does not support interpolants neither?)</p>

<reference-request><linear-temporal-logic>
Craig interpolants for Linear Temporal Logic: finding one when they exist
Nicola Gigante
# Craig interpolants for Linear Temporal Logic: finding one when they exist

(Asked by: username_0 on 2024-09-16)

It is known that Linear Temporal Logic (LTL) does *not* support Craig's theorem, so there are formulas $\phi$ and $\psi$ where $\phi\to\psi$ holds but an interpolant does not exist.

In principle, there may be fragments of LTL supporting interpolation, a trivial special case being the propositional fragment where the original Craig's theorem applies.

However, I've found some literature about the topic and it seems there are not useful proper fragments of LTL supporting interpolation apart from the one with only the *tomorrow* operator which is just syntactic-sugar on top of propositional logic and is not really interesting.

So I cannot have guarantees that an interpolant exists between $\phi$ and $\psi$, however is there an algorithmic way to compute an interpolant *if* it exists?

I'm interested both in LTL on infinite and finite words, if it makes any difference (btw, I don't know if everything above holds for finite words as well: is it true that LTL on finite words does not support interpolants neither?)

**Tags:** reference-request, linear-temporal-logic


---

## 1 answers

### Answer by username_1 on 2024-09-16. Score: 6 | Accepted answer

Decidability of Craig Interpolant Existence for LTL over finite words follows from:

[1] K. Henkell. 1988. Pointlike sets: The finest aperiodic cover of a finite semigroup. Journal of Pure and Applied Algebra
55, 1-2 (1988), 85–126.

[2] K. Henkell, J. Rhodes, and B. Steinberg. 2010. Aperiodic pointlikes and beyond. International Journal of Algebra and
Computation 20, 2 (2010), 287–305,

while the case of omega-word is treated in:

[3] Thomas Place and Marc Zeitoun. 2016. Separating regular languages with first-order logic. Logical Methods in Computer Science 12, 1:5 (2016), 1–30

These results are formulated in terms of the separability problem but CIP Existence and separability are known to be equivalent.

You may also be interested in the following paper:

[4] Jean Christoph Jung, Jedrzej Kolodziejski:
Modal Separability of Fixpoint Formulae. Description Logics 2024

> **Comments:**
> **username_0**: Thank you! That's exactly what I was looking for!  

---

