We study Craig interpolation for fragments and extensions of propositional linear temporal logic (PLTL). We consider various fragments of PLTLobtained 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 PLTLhaving only the Next operator; the extension of PLTLwith a fixpoint operator μ (known as linear time μ-calculus); the fixpoint extension of the "Until-only" fragment of PLTL. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Gheerbrant, A., & Ten Cate, B. (2009). Craig interpolation for linear temporal languages. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5771 LNCS, pp. 287–301). https://doi.org/10.1007/978-3-642-04027-6_22
Mendeley helps you to discover research relevant for your work.