文章基本信息

标题：A Unified Approach to Boundedness Properties in MSO
本地全文：下载
作者：Lukasz Kaiser ; Martin Lang ; Simon Le{\ss}enich 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2015
卷号：41
页码：441-456
DOI：10.4230/LIPIcs.CSL.2015.441
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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. In this work, 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 a decidability proof 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.
关键词：quantitative logics; monadic second order logic; boundedness; automatic structures; tree automata