Deciding the Logic of Subsequences

Level: M2

Contact: Philippe Schnoebelen

The logic of subsequences is the logic of the structure {$(X^*;\leq_*,..)$} where the universe {$X^*$} contains all finite sequences over some base set {$X$}, and where {$\leq_*$} is the subsequence relation (as in Higman's Lemma).

For example, this logic allows writing constraints like {$$ \tag{$\phi$} {aa}\leq_* x \land {bb}\leq_* x \land {ab}\not\leq_* x $$} where {$a,b$} are letters and {$x$} is a variable standing for an unknown word. Over {$X=\{a,b\}$}, the two-letter alphabet, the solution set of the above constraint is the language {$L_\phi={bbb}^*{aaa}^*$}.

The logic allows more complex formulae, like

\begin{equation*} \tag{$\psi$} \forall x,y: \exists z: \bigl( x\leq_* z\land y\leq_* z \land \forall u: x\leq_* u\land y\leq_* u\implies z\leq_* u \bigr) \end{equation*} that states that {$(X^*,\leq_*)$} is an upper semilattice. Whether {$\psi$} is true or false depends on {$X$}.

The goal of this Master Internship is to develop the computational theory of the logic of subsequences, especially by identifying decidable fragments of the logic and assessing their algorithmic complexity.

Until recently, not much was known about the decidability of the logic of subsequences and its fragment [Kus06]. It was then shown that the {$\Sigma_2$} fragment is undecidable (as expected) [KS15], that the {$\mathrm{FO}^2$} fragment is decidable, even elementary [KS16], and that the {$\Sigma_1$}, or existential, fragment is undecidable [HSZ17]. That last result was completely unexpected and has potential far-reaching consequences for existential logics on graphs.

Regarding the {$\mathrm{FO}^2$} fragment, the initial decidability result raised many new questions. In particular there are several interesting directions in which to try to extend the decidability. Among these, the following seem to be good starting points for the M2R internship:

• Extending the decidability of the {$\mathrm{FO}^2$} fragment by allowing combination with other (simple) predicates like {$\leq_{*,1}$} defined via "{$x\leq_{*,1} y$} iff {$x\leq_* y\land |y|=|x|+1$}".
• Extending the logic of subsequences with numerical predicates and (fragments of) Presburger arithmetic.

Another important aspect of [KS16] is that it introduced a new theory of piecewise-complexity as a fundamental tool for establishing elementary upper bounds. This theory need developing and there are many open problems to investigate:

• Algorithmic questions for the piecewise-complexity of words and languages, see e.g. [HS18].
• Extending the theory to trees and other ordered structures.

This research project should suit a theoretically-minded student with some taste for abstract algorithmic constructions like what is encountered in basic courses on recursion theory and computational complexity. It is an ideal opportunity for starting a PhD thesis.

Literature

[HS18]

S. Halfon and Ph. Schnoebelen. On shuffle products, acyclic automata and piecewise-testable languages. Information Processing Letters, 145:68-73, 2019.

[HSZ17]

S. Halfon, Ph. Schnoebelen, and G. Zetzsche. Decidability, complexity, and expressiveness of first-order logic over the subword ordering. In Proc. LICS 2017, pages 1–12. IEEE Comp. Soc. Press, 2017.

[KS15]

P. Karandikar and Ph. Schnoebelen. Decidability in the logic of subsequences and supersequences. In Proc. FST&TCS 2015, volume 45 of LIPICS, pages 84–97. Leibniz-Zentrum für Informatik, 2015.

[KS16]

P. Karandikar and Ph. Schnoebelen. The height of piecewise-testable languages with applications in logical complexity. In Proc. CSL 2016, volume 62 of LIPICS, pages 37 :1–37 :22. Leibniz-Zentrum für Informatik, 2016.

[Kus06]

D. Kuske. Theories of orders on the set of words. RAIRO Theoretical Informatics and Applications, 40(1) :53–74, 2006.