Towards decidable properties of subfragments of quantitative monadic second-order logic

Cristian Riveros

In this talk I will present a new framework for adding quantitative properties to logics over words. We use this framework to define what we called Quantitative Monadic Second-Order Logic (QMSO), an extension of MSO with quantitative operators. By syntactically restricting the nesting of the quantitative operators, we show that this logic has the same expressivenes as weighted automata. Unfortunately, this equivalence implies that many interesting problems (e.g. equivalence and entailment) become undecidable. To avoid these undesirable features of QMSO, one is forced to look at its subfragments and sacrifice expressiveness in favor of decidability. Towards this goal, we show that, by refining the analysis of QMSO, one can obtain subfragments that characterize exactly subclasses of weighted automata defined by the level of ambiguity allowed in the automata.