Logic for \(\omega\)-pushdown automata (Q2064532)

This paper gives a characterization of \(\omega\)-context-free languages in terms of monadic second-order logic. The authors first introduce a notion of \textit{simple \(\omega\)-pushdown automaton} (\(\omega\)SPDA), where the transitions allow only to push/pop a single symbol on the stack or leave the stack unaltered. In order to show that any \(\omega\)-context-free language, as defined in [\textit{R. S. Cohen} and \textit{A. Y. Gold}, J. Comput. Syst. Sci. 15, 169--184 (1977; Zbl 0363.68113)], can be accepted by an \(\omega\)SPDA, the authors use a result of [loc. cit.] to show that that any \(\omega\)-context-free language has a Büchi-accepting grammar in quadratic Greibach normal form. This hence shows the equivalence between \(\omega\)-context-freeness and being recognized by an \(\omega\)SPDA. Furthermore, the authors introduce a monadic second-order logic \(\omega\)ML that uses a (non-overlapping) matching condition on pairs of positions similar to matching parentheses in a well-formed expression. Then, using the fact that their \(\omega\)SPDA are projections of the visibly pushdown automata of [\textit{R. Alur} and \textit{P. Madhusudan}, in: Proceedings of the 36th annual ACM symposium on theory of computing, STOC 2004. New York, NY: ACM Press. 202--211 (2004; Zbl 1192.68396)] and the expressive equivalence result of [\textit{R. Alur} and \textit{P. Madhusudan}, J. ACM 56, No. 3, Article No. 16, 43 p. (2009; Zbl 1325.68138)], they prove the equivalence between \(\omega\)ML-definability and \(\omega\)SPDA-recognizability. This shows that, for an \(\omega\)-language, being \(\omega\)-context-free, \(\omega\)SPDA-recognizable, and \(\omega\)ML-definable are three equivalent notions.