Highly undecidable problems for infinite computations

Finkel, Olivier

Finkel, Olivier

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 43 (2009), p. 339-364 / Harvested from Numdam

Access to full text
Full (PDF)
Full (DJVU)

Résumé

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.

Publié le : 2009-01-01

MR 2512263 | Zbl 1171.03024 | 1 citation dans Numdam

DOI : https://doi.org/10.1051/ita/2009001
Classification: 68Q05, 68Q45, 03D05

@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},
     volume = {43},
     year = {2009},
     pages = {339-364},
     doi = {10.1051/ita/2009001},
     mrnumber = {2512263},
     zbl = {1171.03024},
     language = {en},
     url = {http://dml.mathdoc.fr/item/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) pp. 339-364. doi : 10.1051/ita/2009001. http://gdmltest.u-ga.fr/item/ITA_2009__43_2_339_0/

Bibliographie

[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 1469995 | Zbl 0900.68286

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

[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 2177353 | Zbl 1015.68117

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

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

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

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

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

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

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

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

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

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

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

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

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

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

[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 2250991 | Zbl 1137.03023

[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 1141.68433

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

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

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

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

[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 0495.68063

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

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

[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 645539 | Zbl 0980.68066

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

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

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

[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 1292687

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

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

[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 510641 | Zbl 0387.68050

[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 1718169 | Zbl 0661.03029

[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 1718169 | Zbl 0931.03057

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

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

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

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

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

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

[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 923334 | Zbl 0637.68095

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

[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 1127189 | Zbl 0900.68316