The determinacy strength of pushdown $\omega$-languages

Li, Wenjuan; Tanaka, Kazuyuki

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 51 (2017) no. 1, pp. 29-50.

We investigate the determinacy strength of infinite games whose winning sets are recognized by nondeterministic pushdown automata with various acceptance conditions, e.g., safety, reachability and co-Büchi conditions. In terms of the foundational program “Reverse Mathematics”, the determinacy strength of such games is measured by the complexity of a winning strategy required by the determinacy. Infinite games recognized by nondeterministic pushdown automata have some resemblance to those by deterministic 2-stack visibly pushdown automata with the same acceptance conditions. So, we first investigate the determinacy of games recognized by deterministic 2-stack visibly pushdown automata, together with that by nondeterministic ones. Then, for instance, we prove that the determinacy of games recognized by pushdown automata with a reachability condition is equivalent to the weak König lemma, stating that every infinite binary tree has an infinite path. While the determinacy for pushdown $\omega$-languages with a Büchi condition is known to be independent from ZFC, we here show that for the co-Büchi condition, the determinacy is exactly captured by ATR${}_0$, another popular system of reverse mathematics asserting the existence of a transfinite hierarchy produced by iterating arithmetical comprehension along a given well-order. Finally, we conclude that all results for pushdown automata in this paper indeed hold for 1-counter automata.

R. Alur and P. Madhusudan, Visibly pushdown languages, in Proc. of the 36th Annual ACM Symposium on Theory of Computing, STOC’04 (2004) 202–211. | MR | Zbl

B. Bollig, On the expressive power of 2-stack visibly pushdown automata. Log. Methods Comput. Sci. 4 (2008) 1–35. | DOI | MR | Zbl

J.R. Büchi and L.H. Landweber, Solving sequential conditions by finite-state strategies. Trans. Amer. Math. Soc. 138 (1969) 295–311. | DOI | MR | Zbl

T. Cachat, Higher order pushdown automata, the Caucal hierarchy of graphs and parity games, in International Colloquium on Automata, Languages, and Programming. Springer Berlin Heidelberg (2003) 556–569. | MR | Zbl

T. Cachat, J. Duparc and W. Thomas, Solving pushdown games with a ${\Sigma }_3^0$ winning condition, in International Workshop on Computer Science Logic. Springer Berlin Heidelberg (2002) 322–336. | MR | Zbl

A. Carayol, M. Hague, A. Meyer, C.H. Ong and O. Serre, Winning regions of higher-order pushdown games, in LICS ’08 Proc. of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science (2008) 193–204.

D. Carotenuto, A. Murano and A. Peron, Ordered multi-stack visibly pushdown automata, Theoret. Comput. Sci. 656 (2016) 1–26. | DOI | MR | Zbl

D. Carotenuto, A. Murano and A. Peron, 2-visibly pushdown automata, in International Conference Developments in Language Theory. Springer Berlin Heidelberg (2007) 132–144. | MR | Zbl

R. Chadha, A.P. Sistla and M. Viswanathan, Power of randomization in automata on infinite strings. Log. Methods Comput. Sci. 3 (2011) 1–31. | MR | Zbl

R.S. Cohen and A.Y. Gold, Theory of $\omega$-languages. Part I: Characterization of $\omega$-context-free languages. J. Comput. Syst. Sci. 15 (1977) 169–184. | DOI | MR | Zbl

J. Engelfriet and H.J. Hoogeboom, $X$-automata on $\omega$-words. Theoret. Comput. Sci. 110 (1993) 1–51. | MR | Zbl

O. Finkel, Infinite games specified by 2-tape automata. Ann. Pure Appl. Logic 167 (2016) 1184–1212. | DOI | MR | Zbl

O. Finkel, Topological complexity of context free $\omega$-languages: A survey, in Language, Culture, Computation: Studies in Honor of Yaacov Choueka, vol. 8001 of Lect. Notes Comput. Sci. Springer (2014) 50–77.

O. Finkel, The determinacy of context-free games. J. Symb. Log. 78 (2013) 1115–1134. | DOI | MR | Zbl

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

O. Finkel, On omega context free languages which are Borel sets of infinite rank. Theoret. Comput. Sci. 299 (2003) 327–346. | DOI | MR | Zbl

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

L. Harrington, Analytic determinacy and $0^{♯}$. J. Symb. Log. 43 (1978) 685–693. | DOI | MR | Zbl

D.R. Hirschfeldt, Slicing the truth: On the computable and reverse mathematics of combinatorial principles. In Vol. 28 of Lect. Notes Ser., edited by Institute for Math. Sci., National University of Singapore. World Scientific (2014). | MR | Zbl

E. Jeandel, On immortal configurations in Turing machines, in Conference on Computability in Europe. Vol. 7318 of Lect. Notes Comput. Sci. Springer Berlin Heidelberg (2012) 334–343 | MR | Zbl

C. Löding, P. Madhusudan and O. Serre, Visibly pushdown games, in Proc. of Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2004. Springer Berlin Heidelberg (2005) 408–420. | MR | Zbl

D.A. Martin, Borel determinacy. Ann. Math. 102 (1975) 363–371. | DOI | MR | Zbl

D.A. Martin, Measurable cardinals and analytic games. Fund. Math. 66 (1969/1970) 287–291. | MR | Zbl

M.Y.O. Medsalem and K. Tanaka, ${\Delta }_3^0$-determinacy, comprehension and induction. J. Symb. Log. 72 (2007) 452–462. | DOI | MR | Zbl

A. Montalbán and R.A. Shore, The limits of determinacy in second order arithmetic, in Proc. London Math. Soc. 104 (2012) 223–252. | MR | Zbl

M.L. Minsky, Recursive unsolvability of Post’s problem of tag and other topics in theory of Turing machines. Ann. Math. 74 (1961) 437–455. | DOI | MR | Zbl

M.L. Minsky, Computation: finite and infinite machines. Prentice-Hall, Inc. (1967). | MR | Zbl

T. Nemoto, M.Y. Ould Medsalem and K. Tanaka, Infinite games in the Cantor space and subsystems of second order arithmetic. MLQ Math. Log. Q. 53 (2007) 226–236. | DOI | MR | Zbl

N. Schweber, Transfinite recursion in higher reverse mathematics. J. Symb. Log. 80 (2015) 940–969. | DOI | MR | Zbl

O. Serre, Games with winning conditions of high Borel complexity, in International Colloquium on Automata, Languages, and Programming. Vol. 3142 of Lect. Notes Math. Springer Berlin Heidelberg (2004) 1150–1162. | MR | Zbl

O. Serre, Games with winning conditions of high Borel complexity. Theoret. Comput. Sci. 350 (2006) 345–372. | DOI | MR | Zbl

S.G. Simpson, Subsystems of second order arithmetic. Perspectives in Logic. Association for Symbolic Logic, Poughkeepsie, NY, 2nd edition. Cambridge University Press, Cambridge (2009). | MR | Zbl

L. Staiger, $\omega$-languages,in Chapter 6 of the Handbook of Formal Languages. Vol. 3, edited by G. Rozenberg and A. Salomaa. Springer Verlag, Berlin (1997) 339–387. | MR

J.R. Steel, Determinateness and subsystems of analysis. Ph.D. thesis, University of California, Berkeley (1977). | MR

K. Tanaka, Descriptive set theory and subsystems of analysis. Ph.D. thesis, University of California, Berkeley (1986).

S.L. Torre, M. Napoli and G. Parlato, A unifying approach for multistack pushdown automata.Math. Foundations Comput. Sci. Springer Berlin Heidelberg (2014) 377–389. | MR | Zbl

S.L. Torre, P. Madhusudan and G. Parlato, A robust class of context-sensitive languages, in 22nd Annual IEEE Symposium on Logic in Comput. Sci. IEEE Ph.D. thesis, University (2007) 161–170.

W. Thomas, Infinite games and verification (extended abstract of a tutorial). Lect. Notes Comput. Sci. (2002) 58–64. | Zbl

I. Walukiewicz, Pushdown processes: Games and model-checking, in International Conference on Computer Aided Verification. Springer Berlin Heidelberg (1996) 62–74.

I. Walukiewicz, Pushdown processes: Games and model-checking, Inf. Comput. 164 (2001) 234–263. | DOI | MR | Zbl