Quantitative Monadic Second-Order Logic

While monadic second-order logic is a prominent logic for specifying languages of finite words, it lacks the power to compute quantitative properties, e.g. to count. An automata model capable of computing such properties are weighted automata, but logics equivalent to these automata have only recently emerged. We propose a new framework for adding quantitative properties to logics specifying Boolean properties of words. We use this to define Quantitative Monadic Second-Order Logic (QMSO). In this way we obtain a simple logic which is equally expressive to weighted automata. We analyse its evaluation complexity, both data and combined complexity, and show completeness results for combined complexity. We further refine the analysis of this logic and obtain fragments that characterise exactly subclasses of weighted automata defined by the level of ambiguity allowed in the automata. In this way, we define a quantitative logic which has good decidability properties while being resonably expressive and enjoying a simple syntactical definition.