License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2015.441
URN: urn:nbn:de:0030-drops-54309
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5430/
Go to the corresponding LIPIcs Volume Portal

Kaiser, Lukasz ; Lang, Martin ; Leßenich, Simon ; Löding, Christof

A Unified Approach to Boundedness Properties in MSO

pdf-format:
27.pdf (0.6 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{kaiser_et_al:LIPIcs:2015:5430,
  author =	{Lukasz Kaiser and Martin Lang and Simon Le{\ss}enich and Christof L{\"o}ding},
  title =	{{A Unified Approach to Boundedness Properties in MSO}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{441--456},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Stephan Kreutzer},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5430},
  URN =		{urn:nbn:de:0030-drops-54309},
  doi =		{10.4230/LIPIcs.CSL.2015.441},
  annote =	{Keywords: quantitative logics, monadic second order logic, boundedness, automatic structures, tree automata}
}

Keywords: quantitative logics, monadic second order logic, boundedness, automatic structures, tree automata
Collection: 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Issue Date: 2015
Date of publication: 07.09.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI