Craig Interpolation for Linear Temporal Languages
Amélie Gheerbrant, Balder ten Cate

Abstract:
We study Craig interpolation for fragments and extensions of
propositional linear temporal logic (PLTL). We consider various
fragments of PLTL obtained by restricting the set of temporal
connectives and, for each of these fragments, we identify its smallest
extension that has Craig interpolation. Depending on the underlying
set of temporal operators, this extension turns out to be one of the
following three logics: the fragment of PLTL having only the Next
operator; the extension of PLTL with a fixpoint operator mu (known as
linear time mu-calculus); the fixpoint extension of the "Until-only"
fragment of PLTL.