Logic for ω-pushdown automata

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 Büchi or Muller pushdown automata for infinite words. This extends fundamental logical characterizations of Büchi, Elgot, Trakhtenbrot for regular languages of finite and infinite words and a more recent logical characterization of Lautemann, Schwentick and Thérien 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 Büchi 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.

Authors

• Manfred Droste
• Sven Dziadek
• Werner Kuich

Keywords

• Pushdown automata
• ω-words
• Logic
• Nested-words
• Greibach normal form