RAIRO-Theor. Inf. Appl.
Volume 51, Number 1, January-March 2017
|Page(s)||29 - 50|
|Published online||07 July 2017|
The determinacy strength of pushdown ω-languages∗
Received: 24 July 2016
Accepted: 12 June 2017
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 ω-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 ATR0, 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.
Mathematics Subject Classification: 03D05 / 03B30 / 68Q45
Key words: Gale–Stewart games / pushdown ω-languages / 2-stack visibly pushdown automata / reverse mathematics
© EDP Sciences 2017
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.