A Quantitative Counting Monadic Second-Order Logic

We propose a new quantitative extension of monadic second-order logic, which we call qcMSO, that adds a mechanism to count the size of sets to MSO. We prove that this logic subsumes both MSO+U and costMSO, as for every formula of these logics there is a formula of qcMSO with the same evaluation. Furthermore, central costMSO questions such as boundedness or dominance can be expressed in qcMSO. Using techniques from the field of counter automata, we prove that the weak variant of our logic is decidable on both the infinite linear order and the infinite binary tree, which provides a uniform approach to algorithmic solutions for MSO+U and costMSO problems. Joint work with Łukasz Kaiser (LIAFA, CNRS & Université Paris Diderot - Paris 7) and Martin Lang (Informatik 7, RWTH Aachen University).

Authors

• Simon Leßenich

Keywords

No keywords are indexed for this paper.