The decision problem for some logics for finite words on infinite alphabets

S. Grigorieff   ; Ch. Choffrut

Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part XI, Tome 358 (2008), pp. 100-119

Résumé

This paper is a follow-up of a previous paper where the logical characterization of Eilenberg, Elgot, and Shepherdson of $n$ary synchronous relations was investigated in the case where the alphabet has infinitely many letters. Here we show that modifying one of the predicate leads to a completely different picture for infinite alphabets though it does not change the expressive power for finite alphabets. Indeed, roughly speaking, being able to express the fact that two words end with the same symbol leads to an undecidable theory, already for the $\Sigma_2$ fragment. Finally, we show that the existential fragment is decidable. Bibl. – 19 titles.

Bibliographie

[1] M. Benedikt, L. Libkin, T. Schwentick, L. Ségoufin, “Definable relations and first-order query languages over strings”, J. Ass. Comput. Mach., 50 (2003), 694–751 | MR

[2] M. Bojanczyk, A. Muscholl, T. Schwentick, L. Segoufin, C. David, “Two-variable logic on words with data”, Proceedings of LICS' 06, 2006, 7–16

[3] J. R. Büchi, “On a decision method in restricted second order arithmetics”, Proceedings Int. Cong. in Logic, Methodology and Philosophy of Sci., North-Holland, 1960, 1–11 | MR

[4] C. C. Chang, J. Keisler, Model Theory, North-Holland, 1973 | Zbl

[5] C. Choffrut, S. Grigorieff, “Finite $n$-tape automata over possibly infinite alphabets: extending a theorem of Eilenberg et al.”, Theoret. Comput. Sci., 410:1 (2009), 16–34 | DOI | MR | Zbl

[6] S. Demri, R. Lazić, A. Sangnier, “Model checking freeze LTL over one-counter automata”, Proceedings of FoSSaCS' 08, to appear in Lecture Notes Comp. Sci., 2008 | MR

[7] V. G. Durnev, “Undecidability of the positive $\forall\exists^3$ theory of a free semigroup”, Sib. Mat. Zh., 36:5 (1995), 1067–1080 | DOI | MR | Zbl

[8] S. Eilenberg, C. C. Elgot, J. C. Shepherdson, “Sets recognized by $n$-tape automata”, J. Algebra, 13 (1969), 447–464 | DOI | MR | Zbl

[9] Y. Matiyasevich, G. Senizergues, “Decision problems for semi-thue systems with few rules”, Proceedings 11th LICS 1996 IEEE Computer Soc. Press, 1996, 523–531 | MR

[10] Y. Matiyasevich, G. Senizergues, “Decision problems for semi-thue systems with few rules”, Theor. Comput. Sci., 330:1 (2005), 145–169 | DOI | MR | Zbl

[11] F. Neven, T. Schwentick, V. Vianu, “Towards regular languages over infinite alphabets”, Proceedings 26th MFCS 2001, Lecture Notes Comp. Sci., 2136, 560–572, Extended abstract of [12] | MR | Zbl

[12] F. Neven, T. Schwentick, V. Vianu, “Finite state machines for strings over infinite alphabets”, ACM Transactions on Computational Logic, 15:3 (2004), 403–435 | DOI | MR

[13] B. Poizat, A Course in Model Theory, An Introduction to Modern Mathematical Logic, Universitext, Springer, New York, 2000 | MR

[14] W. Quine, “Concatenation as a basis of arithmetics”, J. Symb. Logic, 11 (1946), 105–114 | DOI | MR | Zbl

[15] J. C. Shepherdson, Unpublished, cited in [17]

[16] J. R. Shoenfield, Mathematical Logic, Addison-Wesley, 1967 | MR | Zbl

[17] J. W. Thatcher, “Decision problems for multiple successor arithmetics”, J. Symb. Logic, 31 (1966), 182–190 | DOI | MR | Zbl

[18] Y. M. Vazhenin, B. V. Rozenblat, “Decidability of the positive theory of a free countably generated semigroup”, Mat. Sb., 116(158) (1981), 120–127 | MR | Zbl

[19] G. Vidal-Naquet, “Quelques applications des automates d'arbres infinis”, Automata, Languages, and Programming, Proceedings ICALP, 1972, ed. M. Nivat, North-Holland, 1972, 115–122 | MR