Automata theory, one of the main branches of theoretical computer science, established its roots in the middle of the 20th century. One of its most fundamental concepts is that of a finite automaton, a basic yet powerful model of computation. In essence, finite automata provide a method to finitely represent possibly infinite sets of strings. Such a set of strings is also called a language, and the languages which can be described by finite automata are known as regular languages. Owing to their versatility, regular languages have received a great deal of attention over the years. Other formalisms were shown to be expressively equivalent to finite automata, most notably regular grammars, regular expressions, and monadic second order (MSO) logic. To increase expressiveness, the fundamental idea underlying finite automata and regular languages was also extended to describe not only languages of strings, or words, but also of infinite words by Büchi and Muller, finite trees by Doner and Thatcher and Wright, infinite trees by Rabin, nested words by Alur and Madhusudan, and pictures by Blum and Hewitt, just to name a few examples. In a parallel line of development, Schützenberger introduced weighted automata which allow the description of quantitative properties of regular languages. In subsequent works, many of these descriptive formalisms and extensions were combined and their relationships investigated. For example, weighted regular expressions and weighted logics have been developed as well as regular expressions for trees and pictures, regular grammars for trees, pictures, and nested words, and logical characterizations for regular languages of trees, pictures, and nested words.
In this work, we focus on two of these extensions and their relationship, namely weighted automata and weighted logics. Just as the classical Büchi-Elgot-Trakhtenbrot Theorem established the coincidence of regular languages with languages definable in monadic second order logic, weighted automata have been shown to be expressively equivalent to a specific fragment of a weighted monadic second order logic by Droste and Gastin. We explore several aspects of weighted automata and of this weighted logic. More precisely, the thesis considers the following topics.
In the first part, we extend the classical Feferman-Vaught Theorem to the weighted setting. The Feferman-Vaught Theorem is one of the fundamental theorems in model theory. The theorem describes how the computation of the truth value of a first order sentence in a generalized product of relational structures can be reduced to the computation of truth values of first order sentences in the contributing structures and the evaluation of an MSO sentence in the index structure. The theorem itself has a long-standing history. It builds upon work of Mostowski, and was shown in subsequent works to hold true for MSO logic. Here, we show that under appropriate assumptions, the Feferman-Vaught Theorem also holds true for a weighted MSO logic with arbitrary commutative semirings as weight structure.
In the second part, we lift four decidability results from max-plus word automata to max-plus tree automata. Max-plus word and tree automata are weighted automata over the max-plus semiring and assign real numbers to words or trees, respectively. We show that, like for max-plus word automata, the equivalence, unambiguity, and sequentiality problems are decidable for finitely ambiguous max-plus tree automata, and that the finite sequentiality problem is decidable for unambiguous max-plus tree automata.
In the last part, we develop a logic which is expressively equivalent to quantitative monitor automata. Introduced very recently by Chatterjee, Henzinger, and Otop, quantitative monitor automata are an automaton model operating on infinite words. Quantitative monitor automata possess several interesting features. They are expressively equivalent to a subclass of nested weighted automata, an automaton model which for many valuation functions has decidable emptiness and universality problems. Also, quantitative monitor automata are more expressive than weighted Büchi-automata and their extension with valuation functions. We introduce a new logic which we call monitor logic and show that it is expressively equivalent to quantitative monitor automata.
| Identifer | oai:union.ndltd.org:DRESDEN/oai:qucosa:de:qucosa:72462 |
| Date | 19 October 2020 |
| Creators | Paul, Erik |
| Contributors | Droste, Manfred, Seidl, Helmut, Universität Leipzig |
| Source Sets | Hochschulschriftenserver (HSSS) der SLUB Dresden |
| Language | English |
| 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.0021 seconds