A unified approach to boundedness properties in MSO

In the past years, extensions of monadic second-order logic (\MSO) that can specify boundedness properties by the use of operators referring to the sizes of sets have been considered. In particular, the logics costMSO introduced by T. Colcombet and MSO+U by M. Bojanczyk were analyzed and connections to automaton models have been established to obtain decision procedures for these logics. We propose the logic quantitative counting MSO (qcMSO for short), which combines aspects from both costMSO and MSO+U. We show that both logics can be embedded into qcMSO in a natural way. Moreover, we provide decidability proofs for the theory of its weak variant (quantification only over finite sets) for the natural numbers with order and the infinite binary tree. These decidability results are obtained using a regular cost function extension of automatic structures called resource-automatic structures. This is joint work with Simon Leßenich, Christof Löding and Lukasz Kaiser. It is currently submitted for publication.

Authors

• Martin Lang

Keywords

No keywords are indexed for this paper.