Logic for ω-pushdown automata

Abstract Context-free languages of infinite words have recently found increasing interest. Here, we will present a second-order logic with the same expressive power as Buchi or Muller pushdown automata for infinite words. This extends fundamental logical characterizations of Buchi, Elgot, Trakhtenbrot for regular languages of finite and infinite words and a more recent logical characterization of Lautemann, Schwentick and Therien for context-free languages of finite words to ω-context-free languages. For our argument, we will investigate Greibach normal forms of ω-context-free grammars as well as a new type of Buchi pushdown automata which can alter their stack by at most one element and without ϵ-transitions. We show that they suffice to accept all ω-context-free languages. This enables us to use similar results recently developed for infinite nested words.