Büchi, Elgot and Trakhtenbrot provided a seminal connection between monadic second-order logic and finite automata for both finite and infinite words. This BET- Theorem has been extended by Lautemann, Schwentick and Thérien to context-free languages by introducing a monadic second-order logic with an additional existentially quantified second-order variable. This new variable models the stack of pushdown au- tomata. A fundamental study by Cohen and Gold extended the context-free languages to infinite words. Our first main result is a second-order logic in the sense of Lautemann, Schwentick and Thérien with the same expressive power as ω-context-free languages. For our argument, we investigate Greibach normal forms of ω-context-free grammars as well as a new type of Büchi pushdown automata, the simple pushdown automata. Simple pushdown automata do not use e-transitions and can change the stack only by at most one symbol. We show that simple pushdown automata of infinite words suffice to accept all ω-context-free languages. This enables us to use Büchi-type results recently developed for infinite nested words.
In weighted automata theory, many classical results on formal languages have been extended into a quantitative setting. Weighted context-free languages of finite words trace back already to Chomsky and Schützenberger. Their work has been extended to infinite words by Ésik and Kuich. As in the theory of formal grammars, these weighted ω-context-free languages, or ω-algebraic series, can be represented as solutions of mixed ω-algebraic systems of equations and by weighted ω-pushdown automata.
In our second main result, we show that (mixed) ω-algebraic systems can be trans- formed into Greibach normal form.
We then investigate simple pushdown automata in the weighted setting. Here, we give our third main result. We prove that weighted simple pushdown automata of finite words recognize all weighted context-free languages, i.e., generate all algebraic series. Then, we show that weighted simple ω-pushdown automata generate all ω-algebraic series. This latter result uses the former result together with the Greibach normal form that we developed for ω-algebraic systems.
As a fourth main result, we prove that for weighted simple ω-pushdown automata, Büchi-acceptance and Muller-acceptance are expressively equivalent.
In our fifth main result, we derive a Nivat-like theorem for weighted simple ω- pushdown automata. This theorem states that the behaviors of our automata are precisely the projections of very simple ω-series restricted to ω-context-free languages.
The last result, our sixth main result, is a weighted logic with the same expressive power as weighted simple ω-pushdown automata. To prove the equivalence, we use a similar result for weighted nested ω-word automata and apply our present result of expressive equivalence of Muller and Büchi acceptance.
| Identifer | oai:union.ndltd.org:DRESDEN/oai:qucosa:de:qucosa:74243 |
| Date | 26 March 2021 |
| Creators | Dziadek, Sven |
| Contributors | Droste, Manfred, Kuich, Werner, Droste, Manfred, Kuich, Werner, Honkala, Juha, Universität Leipzig |
| Source Sets | Hochschulschriftenserver (HSSS) der SLUB Dresden |
| Language | English, German |
| Detected Language | English |
| Type | info:eu-repo/semantics/acceptedVersion, doc-type:doctoralThesis, info:eu-repo/semantics/doctoralThesis, doc-type:Text |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.002 seconds