Document Open Access Logo

A Unified Approach to Boundedness Properties in MSO

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

PDF
Thumbnail PDF

File

LIPIcs.CSL.2015.441.pdf
  • Filesize: 0.56 MB
  • 16 pages

Document Identifiers

Author Details

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

Cite As Get BibTex

Lukasz Kaiser, Martin Lang, Simon Leßenich, and Christof Löding. A Unified Approach to Boundedness Properties in MSO. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 441-456, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CSL.2015.441

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.

Subject Classification

Keywords
  • quantitative logics
  • monadic second order logic
  • boundedness
  • automatic structures
  • tree automata

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. A. Blumensath. Automatic Structures. Diploma thesis, RWTH-Aachen, 1999. Google Scholar
  2. A. Blumensath and E. Grädel. Automatic Structures. In LICS 2000, pages 51-62, 2000. Google Scholar
  3. M. Bojanczyk. Weak MSO with the Unbounding Quantifier. In STACS 09, volume 3, pages 159-170, 2009. Google Scholar
  4. M. Bojańczyk. Weak MSO with the unbounding quantifier. Theory of Computing Systems, 48(3):554-576, 2011. Google Scholar
  5. M. Bojańczyk, T. Gogacz, H. Michalewski, and M. Skrzypczak. On the decidability of MSO+U on infinite trees. In Automata, Languages, and Programming, volume 8573 of LNCS, pages 50-61. Springer, 2014. Google Scholar
  6. M. Bojańczyk, P. Parys, and S. Toruńczyk. The MSO+U theory of (ℕ, <) is undecidable. arXiv:1502.04578 [cs.LO], 2015. Google Scholar
  7. M. Bojanczyk and S. Torunczyk. Weak MSO+U over infinite trees. In STACS 2012, volume 14, pages 648-660, Dagstuhl, Germany, 2012. Google Scholar
  8. M. Bojańczyk and S. Toruńczyk. Weak MSO+U over infinite trees. In Christoph Dürr and Thomas Wilke, editors, STACS 2012, volume 14, pages 648-660, 2012. Google Scholar
  9. T. Colcombet. Regular cost functions over words. Manuscript available online, 2009. Google Scholar
  10. T. Colcombet. The theory of stabilisation monoids and regular cost functions. In Automata, Languages and Programming, volume 5556 of LNCS, pages 139-150. Springer, 2009. Google Scholar
  11. T. Colcombet. Regular cost functions, part I: logic and algebra over words. Logical Methods in Computer Science, 9(3), 2013. Google Scholar
  12. T. Colcombet and C. Löding. Regular cost functions over finite trees. In LICS 2010, pages 70-79, July 2010. Google Scholar
  13. H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications. Available online: http://www.grappa.univ-lille3.fr/tata, 2007. release October, 12th 2007.
  14. D. Fischer, E. Grädel, and Ł. Kaiser. Model Checking Games for the Quantitative mu-Calculus. Theory Comput. Syst., 47(3):696-719, 2010. Google Scholar
  15. S. Hummel and M. Skrzypczak. The topological complexity of MSO+U and related automata models. Fundamenta Informaticae, 119(1):87-111, 2012. Google Scholar
  16. B. Khoussainov and A. Nerode. Automatic presentations of structures. In Logic and Computational Complexity, volume 960 of LNCS, pages 367-392. Springer, 1995. Google Scholar
  17. D. Kuperberg and M. Vanden Boom. On the expressive power of cost logics over infinite words. In ICALP 2012, volume 7392 of LNCS, pages 287-298. Springer, 2012. Google Scholar
  18. M. Lang and C. Löding. Modeling and verification of infinite systems with resources. Logical Methods in Computer Science, 9(4), 2013. Google Scholar
  19. M. Lang, C. Löding, and A. Manuel. Definability and transformations for cost logics and automatic structures. In MFCS 2014, volume 8634 of LNCS, pages 390-401. Springer, 2014. Google Scholar
  20. W. Thomas. Languages, automata, and logic. In Handbook of Formal Language Theory, volume III, pages 389-455. Springer, 1997. Google Scholar
  21. M. Vanden Boom. Weak cost monadic logic over infinite trees. In MFCS 2011, volume 6907 of LNCS, pages 580-591. Springer, 2011. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact