Decidability in the Logic of Subsequences and Supersequences

Authors Prateek Karandikar, Philippe Schnoebelen

Thumbnail PDF


  • Filesize: 497 kB
  • 14 pages

Document Identifiers

Author Details

Prateek Karandikar
Philippe Schnoebelen

Cite AsGet BibTex

Prateek Karandikar and Philippe Schnoebelen. Decidability in the Logic of Subsequences and Supersequences. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 84-97, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


We consider first-order logics of sequences ordered by the subsequence ordering, aka sequence embedding. We show that the Sigma_2 theory is undecidable, answering a question left open by Kuske. Regarding fragments with a bounded number of variables, we show that the FO^2 theory is decidable while the FO^3 theory is undecidable.
  • subsequence
  • subword
  • logic
  • first-order logic
  • decidability
  • piecewise- testability
  • Simon’s congruence


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. P. A. Abdulla, M. Faouzi Atig, Yu-Fang Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman. String constraints for verification. In Proc. CAV 2014, volume 8559 of Lecture Notes in Computer Science, pages 150-166. Springer, 2014. Google Scholar
  2. P. A. Abdulla, A. Collomb-Annichini, A. Bouajjani, and B. Jonsson. Using forward reachability analysis for verification of lossy channel systems. Formal Methods in System Design, 25(1):39-65, 2004. Google Scholar
  3. J. Berstel. Transductions and Context-Free Languages. B. G. Teubner, Stuttgart, 1979. Google Scholar
  4. P. Bouyer, N. Markey, J. Ouaknine, Ph. Schnoebelen, and J. Worrell. On termination and invariance for faulty channel machines. Formal Aspects of Computing, 24(4-6):595-607, 2012. Google Scholar
  5. H. Comon. Solving symbolic ordering constraints. Int. J. Foundations of Computer Science, 1(4):387-412, 1990. Google Scholar
  6. H. Comon and R. Treinen. Ordering constraints on trees. In Proc. CAAP '94, volume 787 of Lecture Notes in Computer Science, pages 1-14. Springer, 1994. Google Scholar
  7. V. Ganesh, M. Minnes, A. Solar-Lezama, and M. C. Rinard. Word equations with length constraints: What’s decidable? In Proc. HVC 2012, volume 7857 of Lecture Notes in Computer Science, pages 209-226. Springer, 2013. Google Scholar
  8. Ch. Haase, S. Schmitz, and Ph. Schnoebelen. The power of priority channel systems. Logical Methods in Comp. Science, 10(4:4), 2014. Google Scholar
  9. J. Harrison. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009. Google Scholar
  10. P. Hooimeijer and W. Weimer. StrSolve: solving string constraints lazily. Autom. Softw. Eng., 19(4):531-559, 2012. Google Scholar
  11. P. Karandikar and Ph. Schnoebelen. Generalized Post embedding problems. Theory of Computing Systems, 56(4):697-716, 2015. Google Scholar
  12. D. Kuske. Theories of orders on the set of words. RAIRO Theoretical Informatics and Applications, 40(1):53-74, 2006. Google Scholar
  13. D. Kuske. Private email exchanges, April 2014. Google Scholar
  14. J. Sakarovitch. Elements of Automata Theory. Cambridge University Press, 2009. Google Scholar
  15. J. Sakarovitch and I. Simon. Subwords. In M. Lothaire, editor, Combinatorics on words, volume 17 of Encyclopedia of Mathematics and Its Applications, chapter 6, pages 105-142. Cambridge Univ. Press, 1983. Google Scholar
  16. I. Simon. Piecewise testable events. In Proc. 2nd GI Conf. on Automata Theory and Formal Languages, volume 33 of Lecture Notes in Computer Science, pages 214-222. Springer, 1975. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail