Craig Interpolation for Linear Temporal Languages

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 µ (known as linear time µ-calculus); the fixpoint extension of the “Until-only” fragment of PLTL. Key words: Propositional Linear Temporal Logic, Craig Interpolation, Linear Time µ-Calculus

• Type: Conference
• Year: 2009
• Where: CSL
• Authors: Amélie Gheerbrant, Balder ten Cate
• Keywords: Artificial Intelligence, Craig Interpolation, CSL 2009, Linear Temporal Logic, Propositional Linear