Interpolation and Separation Problems for Linear Temporal Logics

This talk discusses two types of problems that have recently been posed and investigated in the context of linear time temporal logics.

The first problem is related to Craig interpolation. Recall that a logic $L$ has the Craig interpolation property (CIP, for short) if, for any two formulas $\phi$ and $\psi$ in the language of $L$, whenever $\phi \to \psi$ is valid in $L$, then there exists a formula $\chi$, constructed from the common non-logical symbols of $\phi$ and $\psi$, such that both $\phi \to \chi$ and $\chi \to \psi$ are valid in $L$. Such a formula $\chi$ is called an interpolant of $\phi$ and $\psi$ in $L$. Classical and intuitionistic propositional and first-order logics, standard modal and description logics as well as numerous other logics enjoy the CIP. The vast majority of temporal logics do not, including all logics with the operators $\mathrm{◇}$ (some time in the future) and $\mathrm{\square }$ (always in the future) interpreted over any class of connected Kripke frames of unbounded depth, their Priorean extensions with the past-time operators, and full linear temporal logic $\mathrm{𝖫𝖳𝖫}$ over any interesting time line.

A different, non-uniform approach to Craig interpolation in logics $L$ without the CIP was suggested in [4] by posing the following interpolant existence problem (IEP): given any formulas $\phi$ and $\psi$ in the language of $L$, decide whether there exists an interpolant $\chi$ for $\phi$ and $\psi$ in $L$. For $L$ with the CIP, interpolant existence reduces to validity; for $L$ without the CIP, the IEP is typically harder as far as computational complexity is concerned.

The first part of the talk gives a survey of the recent results on the IEP in temporal logics obtained in [5, 6]. In particular, it discusses how a semantic criterion of interpolant existence in terms of descriptive frames can be used to design a coNP-algorithm that is capable of deciding the IEP for any given finitely axiomatisable temporal logic with the operators $\mathrm{◇}$ and $\mathrm{\square }$. In this case, the IEP is as complex as the decision problem for the logic. For $\mathrm{𝖫𝖳𝖫}$ over finite strict linear orders, the talk discusses how the IEP can be reduced to the following separation problem: given two regular languages ${ℒ}_1$ and ${ℒ}_2$, decide whether there is a first-order definable (= star-free) language $ℒ$ separating ${ℒ}_1$ and ${ℒ}_2$ in the sense that ${ℒ}_1\subseteq ℒ$ and ${ℒ}_2\cap ℒ=\mathrm{\varnothing }$. A classical result of [7] shows that deciding first-order separability of two regular languages is in $2\text{ExpTime}$ in the size of the DFAs specifying the given languages. Thus, the IEP for $\mathrm{𝖫𝖳𝖫}$ is decidable in $4\text{ExpTime}$, being PSpace-hard. The same bounds hold for $\mathrm{𝖫𝖳𝖫}$ over . In both cases, the exact complexity remains open.

The second part of the talk is concerned with the scenario where temporal models over finite strict linear orders represent timestamped (qualitative) data. We discuss the reverse engineering (or query-by-example) setting that deals with pairs $(E^{+},E^{-})$ of finite sets of “positive” and “negative” data examples. An $\mathrm{𝖫𝖳𝖫}$-formula (query) $𝒒$ separates $(E^{+},E^{-})$ if $𝔐,0\vDash 𝒒$ for all $𝔐\in E^{+}$, and $𝔐,0\vDash ̸𝒒$ for all $𝔐\in E^{-}$. Based on the results from [1, 2, 3], we give a survey of recent developments in the study of the following problems:

Given any pair $(E^{+},E^{-})$ of positive and negative examples and a class $𝒬$ of $\mathrm{𝖫𝖳𝖫}$-queries,

1. 1.

   How hard is it to decide whether $(E^{+},E^{-})$ is separable by a query in $𝒬$?

2. 2.

   How hard is it to compute a $𝒬$-separator of $(E^{+},E^{-})$, which is $(i)$ shortest/longest or $(ii)$ most specific (logically strongest)/most general (weakest) $𝒬$-separator?

3. 3.

   How hard is it to decide whether there is a unique most specific/general $𝒬$-separator?

4. 4.

   Given a $𝒬$-separator $𝒒$ of $(E^{+},E^{-})$, how hard is it to decide whether $𝒒$ is $(i)$ shortest/ longest, $(ii)$ most general/specific, $(iii)$ unique, etc.?

5. 5.

   Given any $𝒒\in 𝒬$, how hard is it to decide whether there is $(E^{+},E^{-})$ that uniquely characterises $𝒒$ in $𝒬$ in the sense that ${𝒒}^{\prime }\in 𝒬$ separates $(E^{+},E^{-})$ iff ${𝒒}^{\prime }\equiv 𝒒$?

6. 6.

   Does there exist a polynomial-size unique characterisation of a given $𝒒\in 𝒬$?

Interesting and practically relevant classes $𝒬$ consist of conjunctive $\mathrm{𝖫𝖳𝖫}$ formulas. We also outline generalisations of the problems above to combinations of $\mathrm{𝖫𝖳𝖫}$ and description logics.