Tutorial: Weighted Automata: Highlighted Excerpts

This talk will focus on a few highlights from the huge theory of weighted automata (WA). First, we introduce weighted automata and show how they can be used to model quantitative aspects of systems. This model is extremely versatile and by varying the weights/computations it can be used to describe counting, probabilities, optimizations, average power consumption, etc. We focus on sequential finite behaviors (words), and quickly discuss a few extensions (infinite words, trees, pebble-walking automata). We also investigate a few decision problems: emptiness, threshold, equivalence, recognizability of the support, etc. Second, we concentrate on weights/computations arising from a semiring. Actually, weighted automata were originally studied in this setting only, giving rise to an extensive theory of WA and formal power series (FPS), i. e. , quantitative functions over words. This special case allows for specific algorithms/definitions/results. For instance, a weighted automaton can be represented by a morphism to the monoid of matrices. The value/semantics of a WA can be computed efficiently using products of vectors/matrices (linear in the size of the input word, quadratic in the size of the automaton). Further, when the semiring is a field (possibly non-commutative), we will explain how to minimize a WA. As a consequence, the equivalence problem is decidable for WA over a subsemiring of a field. Last, the semiring structure allows one to define a (Cauchy) product of FPS and to obtain the equivalence between functions (FPS) that can be computed by WA and functions that can be denoted by weighted rational expressions. This extension of Kleene’s result is known as Schützenberger's theorem. Third, we will survey how weighted logics have been developed to match the quantitative expressive power of WA. The story started 10 years ago with the introduction of a quantitative (semiring) semantics for MSO logic over finite words and an equivalence theorem between weighted automata and a restricted weighted MSO logic. Since then, many extensions have been studied. Some extend the structure from words to trees, infinite words, pictures, etc. Others concern the quantitative aspect, moving from semirings to more general weights/computations. Also, the proof techniques have matured, from low level, carefully mimicking the classical proofs in the boolean setting, to higher level, using various abstract semantics. We illustrate this evolution by introducing a core weighted logic and its abstract semantics as multisets of weight structures. The equivalence between weighted automata and core weighted logic holds at the level of the abstract semantics. Most existing results can be derived easily.

Authors

• Paul Gastin

Keywords

No keywords are indexed for this paper.