LIPIcs.FSTTCS.2015.84.pdf
- Filesize: 497 kB
- 14 pages
Document
Decidability in the Logic of Subsequences and Supersequences
Authors
-
Part of:
Volume:
35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2015-12-14
Cite As Get 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)
https://doi.org/10.4230/LIPIcs.FSTTCS.2015.84
Abstract
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.
Subject Classification
Keywords
- subsequence
- subword
- logic
- first-order logic
- decidability
- piecewise- testability
- Simon’s congruence
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
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.
-
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.
-
J. Berstel. Transductions and Context-Free Languages. B. G. Teubner, Stuttgart, 1979.
-
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.
-
H. Comon. Solving symbolic ordering constraints. Int. J. Foundations of Computer Science, 1(4):387-412, 1990.
-
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.
-
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.
-
Ch. Haase, S. Schmitz, and Ph. Schnoebelen. The power of priority channel systems. Logical Methods in Comp. Science, 10(4:4), 2014.
-
J. Harrison. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009.
-
P. Hooimeijer and W. Weimer. StrSolve: solving string constraints lazily. Autom. Softw. Eng., 19(4):531-559, 2012.
-
P. Karandikar and Ph. Schnoebelen. Generalized Post embedding problems. Theory of Computing Systems, 56(4):697-716, 2015.
-
D. Kuske. Theories of orders on the set of words. RAIRO Theoretical Informatics and Applications, 40(1):53-74, 2006.
-
D. Kuske. Private email exchanges, April 2014.
-
J. Sakarovitch. Elements of Automata Theory. Cambridge University Press, 2009.
-
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.
-
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.