Highly undecidable problems for infinite computations
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 43 (2009) no. 2, pp. 339-364.

We show that many classical decision problems about 1-counter ω-languages, context free ω-languages, or infinitary rational relations, are Π 2 1 -complete, hence located at the second level of the analytical hierarchy, and “highly undecidable”. In particular, the universality problem, the inclusion problem, the equivalence problem, the determinizability problem, the complementability problem, and the unambiguity problem are all Π 2 1 -complete for context-free ω-languages or for infinitary rational relations. Topological and arithmetical properties of 1-counter ω-languages, context free ω-languages, or infinitary rational relations, are also highly undecidable. These very surprising results provide the first examples of highly undecidable problems about the behaviour of very simple finite machines like 1-counter automata or 2-tape automata.

DOI : 10.1051/ita/2009001
Classification : 68Q05, 68Q45, 03D05
Mots clés : infinite computations, $1$-counter-automata, $2$-tape automata, decision problems, arithmetical hierarchy, analytical hierarchy, complete sets, highly undecidable problems
@article{ITA_2009__43_2_339_0,
     author = {Finkel, Olivier},
     title = {Highly undecidable problems for infinite computations},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {339--364},
     publisher = {EDP-Sciences},
     volume = {43},
     number = {2},
     year = {2009},
     doi = {10.1051/ita/2009001},
     mrnumber = {2512263},
     zbl = {1171.03024},
     language = {en},
     url = {http://www.numdam.org/articles/10.1051/ita/2009001/}
}
TY  - JOUR
AU  - Finkel, Olivier
TI  - Highly undecidable problems for infinite computations
JO  - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 2009
SP  - 339
EP  - 364
VL  - 43
IS  - 2
PB  - EDP-Sciences
UR  - http://www.numdam.org/articles/10.1051/ita/2009001/
DO  - 10.1051/ita/2009001
LA  - en
ID  - ITA_2009__43_2_339_0
ER  - 
%0 Journal Article
%A Finkel, Olivier
%T Highly undecidable problems for infinite computations
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 2009
%P 339-364
%V 43
%N 2
%I EDP-Sciences
%U http://www.numdam.org/articles/10.1051/ita/2009001/
%R 10.1051/ita/2009001
%G en
%F ITA_2009__43_2_339_0
Finkel, Olivier. Highly undecidable problems for infinite computations. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 43 (2009) no. 2, pp. 339-364. doi : 10.1051/ita/2009001. http://www.numdam.org/articles/10.1051/ita/2009001/

[1] J.-M. Autebert, J. Berstel and L. Boasson, Context free languages and pushdown automata, in Handbook of formal languages, Vol. 1. Springer-Verlag (1996). | MR | Zbl

[2] R. Alur and D.L. Dill, A theory of timed automata. Theoret. Comput. Sci. 126 (1994) 183-235. | MR | Zbl

[3] J.-H. Altenbernd, W. Thomas and S. Wöhrle, Tiling systems over infinite pictures and their acceptance conditions, in Proceedings of the 6th International Conference Developments in Language Theory, DLT 2002. Lect. Notes Comput. Sci. 2450 (2003) 297-306. | MR | Zbl

[4] J. Berstel, Transductions and context free languages. Teubner Studienbücher Informatik (1979). | MR | Zbl

[5] J. Castro and F. Cucker, Nondeterministic ω-computations and the analytical hierarchy. Z. Math. Logik Grundlagen Math 35 (1989) 333-342. | MR | Zbl

[6] R.S. Cohen and A.Y. Gold, Theory of ω-languages, parts one and two. J. Comput. System. Sci. 15 (1977) 169-208. | MR | Zbl

[7] R.S. Cohen and A.Y. Gold, ω-computations on deterministic pushdown machines. J. Comput. System. Sci. 16 (1978) 275-300. | MR | Zbl

[8] R.S. Cohen and A.Y. Gold, ω-computations on Turing machines. Theoret. Comput. Sci. 6 (1978) 1-23. | MR | Zbl

[9] P. Darondeau and S. Yoccoz, Proof systems for infinite behaviours. Inform. Comput. 99 (1992) 178-191. | MR | Zbl

[10] J. Engelfriet and H.J. Hoogeboom, X-automata on ω-words. Theoret. Comput. Sci. 110 (1993) 1-51. | MR | Zbl

[11] O. Finkel, Topological properties of omega context free languages. Theoret. Comput. Sci. 262 (2001) 669-697. | MR | Zbl

[12] O. Finkel, Ambiguity in omega context free languages. Theoret. Comput. Sci. 301 (2003) 217-270. | MR | Zbl

[13] O. Finkel, Borel hierarchy and omega context free languages. Theoret. Comput. Sci. 290 (2003) 1385-1405. | MR | Zbl

[14] O. Finkel, On the topological complexity of infinitary rational relations. RAIRO-Theor. Inf. Appl. 37 (2003) 105-113. | Numdam | MR | Zbl

[15] O. Finkel, Undecidability of topological and arithmetical properties of infinitary rational relations. RAIRO-Theor. Inf. Appl. 37 (2003) 115-126. | Numdam | MR | Zbl

[16] O. Finkel, On recognizable languages of infinite pictures. Int. J. Found. Comput. Sci. 15 (2004) 823-840. | MR | Zbl

[17] O. Finkel, Borel ranks and Wadge degrees of omega context free languages. Math. Struct. Comput. Sci. 16 (2006) 813-840. | MR | Zbl

[18] O. Finkel, On the accepting power of two-tape Büchi automata, in Proceedings of the 23rd International Symposium on Theoretical Aspects of Computer Science, STACS 2006. Lect. Notes Comput. Sci. 3884 (2006) 301-312. | MR | Zbl

[19] O. Finkel, Undecidable problems about timed automata, in Proceedings of the 4th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2006. Lect. Notes Comput. Sci. 4202 (2006) 187-199. | Zbl

[20] O. Finkel, Highly undecidable problems about recognizability by tiling systems. Fundamenta Informaticae, 2009. Special Issue on Machines, Computations and Universality (to appear). | MR

[21] O. Finkel and D. Lecomte. Classical and effective descriptive complexities of omega-powers (2007). Preprint http://fr.arxiv.org/abs/0708.4176. | Zbl

[22] C. Frougny and J. Sakarovitch, Synchronized rational relations of finite and infinite words. Theoret. Comput. Sci. 108 (1993) 45-82. | MR | Zbl

[23] O. Finkel and P. Simonnet, Topology and ambiguity in omega context free languages. Bull. Belg. Math. Soc. 10 (2003) 707-722. | MR | Zbl

[24] F. Gire, Relations rationnelles infinitaires. Ph.D. thesis, Université Paris VII (1981).

[25] F. Gire, Une extension aux mots infinis de la notion de transduction rationelle, in Theoretical Computer Science, 6th GI-Conference, Dortmund, Germany, January 5-7, 1983, Proceedings. Lect. Notes Comput. Sci. 145 (1983) 123-139. | Zbl

[26] F. Gire and M. Nivat, Relations rationnelles infinitaires. Calcolo (1984) 91-125. | MR | Zbl

[27] T. Harju and J. Karhumäki. The equivalence problem of multitape finite automata. Theoret. Comput. Sci. 78 (1991) 347-355. | MR | Zbl

[28] J.E. Hopcroft, R. Motwani and J.D. Ullman, Introduction to automata theory, languages, and computation. Addison-Wesley Publishing Co., Reading, Mass. (2001). Addison-Wesley Series in Computer Science. | MR | Zbl

[29] A.S. Kechris, Classical descriptive set theory. Springer-Verlag, New York (1995). | MR | Zbl

[30] L.H. Landweber, Decision problems for ω-automata. Math. Syst. Theor. 3 (1969) 376-384. | MR | Zbl

[31] M. Linna, On ω-words and ω-computations. Ann. Univ. Turku. Ser A I 168 (1975) 53. | MR | Zbl

[32] H. Lescow and W. Thomas, Logical specifications of infinite computations, in A Decade of Concurrency, edited by J.W. de Bakker, Willem P. de Roever and Grzegorz Rozenberg. Lect. Notes Comput. Sci. 803 (1994) 583-621. | MR

[33] Y.N. Moschovakis, Descriptive set theory. North-Holland Publishing Co., Amsterdam (1980). | MR | Zbl

[34] M. Nivat, Mots infinis engendrés par une grammaire algébrique. RAIRO-Inf. Théor. Appl. 11 (1977) 311-327. | Numdam | MR | Zbl

[35] M. Nivat, Sur les ensembles de mots infinis engendrés par une grammaire algébrique. RAIRO-Inf. Théor. Appl. 12 (1978) 259-278. | Numdam | MR | Zbl

[36] P.G. Odifreddi, Classical Recursion Theory, Vol I, Studies in Logic and the Foundations of Mathematics, Vol. 125. North-Holland Publishing Co., Amsterdam (1989). | MR | Zbl

[37] P.G. Odifreddi, Classical Recursion Theory, Vol II, Studies in Logic and the Foundations of Mathematics, Vol. 143. North-Holland Publishing Co., Amsterdam (1999). | MR | Zbl

[38] D. Perrin and J.-E. Pin, Infinite words, automata, semigroups, logic and games, Pure and Applied Mathematics, Vol. 141. Elsevier (2004). | Zbl

[39] A. Prasad Sistla, On verifying that a concurrent program satisfies a nondeterministic specification. Inform. Process. Lett. 32 (1989) 17-23. | MR | Zbl

[40] H. Rogers, Theory of Recursive Functions and Effective Computability. McGraw-Hill, New York (1967). | MR | Zbl

[41] G. Sénizergues, L(A) = L(B)? decidability results from complete formal systems. Theoret. Comput. Sci. 251 (2001) 1-166. | MR | Zbl

[42] P. Simonnet, Automates et théorie descriptive. Ph.D. thesis, Université Paris VII (1992). | JFM

[43] L. Staiger, Hierarchies of recursive ω-languages. Elektronische Informationsverarbeitung und Kybernetik 22 (1986) 219-241. | MR | Zbl

[44] L. Staiger, Research in the theory of ω-languages. J. Inf. Process. Cybernetics 23 (1987) 415-439. Mathematical aspects of informatics (Mägdesprung, 1986). | MR | Zbl

[45] L. Staiger, ω-languages, in Handbook of formal languages, Vol. 3. Springer, Berlin (1997) 339-387. | MR

[46] W. Thomas, Automata on infinite objects, in Handbook of Theoretical Computer Science, Vol. B, Formal models and semantics, edited by J. van Leeuwen. Elsevier (1990) 135-191. | MR | Zbl

Cité par Sources :