Document Open Access Logo

Monadic Second Order Finite Satisfiability and Unbounded Tree-Width

Authors Tomer Kotek, Helmut Veith, Florian Zuleger

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2016.13.pdf
  • Filesize: 0.61 MB
  • 20 pages

Document Identifiers

Subject Classification

Keywords
  • Monadic Second Order Logic MSO
  • Two variable Fragment with Counting C2
  • Finite decidability
  • Unbounded Tree-width
  • WS1S with Cardinality Constraints

Metrics

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

Abstract

The finite satisfiability problem of monadic second order logic is decidable only on classes of structures of bounded tree-width by the classic result of Seese. We prove that the following problem is decidable:

Input: (i) A monadic second order logic sentence alpha, and (ii) a sentence beta in the two-variable fragment of first order logic extended with counting quantifiers. The vocabularies of alpha and beta may intersect.

Output: Is there a finite structure which satisfies alpha and beta such that the restriction of the structure to the vocabulary of alpha has bounded tree-width? (The tree-width of the desired structure is not bounded.)

As a consequence, we prove the decidability of the satisfiability problem by a finite structure of bounded tree-width of a logic MS^{exists card} extending monadic second order logic with linear cardinality constraints of the form |X_{1}|+...+|X_{r}| < |Y_{1}|+...+|Y_{s}| on the variables X_i, Y_j of the outer-most quantifier block. We prove the decidability of a similar extension of WS1S.

Cite As Get BibTex

Tomer Kotek, Helmut Veith, and Florian Zuleger. Monadic Second Order Finite Satisfiability and Unbounded Tree-Width. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 13:1-13:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.CSL.2016.13

Author Details

Tomer Kotek
Helmut Veith
Florian Zuleger

References

  1. S. Arnborg, J. Lagergren, and D. Seese. Easy problems for tree-decomposable graphs. Journal of Algorithms, 12(2):308-340, 1991. Google Scholar
  2. F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, and P. F. Patel-Schneider, editors. The Description Logic handbook. Cambridge University Press, 2003. Google Scholar
  3. D. Calvanese, T. Kotek, M. Šimkus, H. Veith, and F. Zuleger. Shape and content. In Integrated Formal Methods, pages 3-17. Springer, 2014. Google Scholar
  4. W. Charatonik and P. Witkowski. Two-variable logic with counting and trees. In LICS, pages 73-82. IEEE, 2013. Google Scholar
  5. B. Courcelle. The monadic second-order logic of graphs. i. recognizable sets of finite graphs. Information and computation, 85(1):12-75, 1990. Google Scholar
  6. B. Courcelle and J. Engelfriet. Graph structure and monadic second-order logic: a language-theoretic approach, volume 138. Cambridge University Press, 2012. Google Scholar
  7. B. Courcelle and J. A. Makowsky. Fusion in relational structures and the verification of monadic second-order properties. Mathematical Structures in Computer Science, 12(02):203-235, 2002. Google Scholar
  8. J. Flum and M. Grohe. Parameterized Complexity Theory. Texts in Theoretical Computer Science. Springer, 2006. Google Scholar
  9. E. Grädel. On the restraining power of guards. The Journal of Symbolic Logic, 64(04):1719-1742, 1999. Google Scholar
  10. E. Grädel and M. Otto. On logics with two variables. Theoretical computer science, 224(1):73-113, 1999. Google Scholar
  11. E. Grädel, M. Otto, and E. Rosen. Two-variable logic with counting is decidable. In LICS, pages 306-317. IEEE, 1997. Google Scholar
  12. Erich Grädel, Martin Otto, and Eric Rosen. Undecidability results on two-variable logics. In STACS 97, 14th Annual Symposium on Theoretical Aspects of Computer Science, Lübeck, Germany, February 27 - March 1, 1997, Proceedings, pages 249-260, 1997. Google Scholar
  13. J.G. Henriksen, J. Jensen, M. Jørgensen, N. Klarlund, R. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. Springer, 1995. Google Scholar
  14. W. Hodges. Model theory. In Encyclopedia of Mathematics and its Applications, volume 42. Cambridge University Press, 1993. Google Scholar
  15. F. Klaedtke and H. Rueß. Monadic second-order logics with cardinalities. In Automata, Languages and Programming, pages 681-696. Springer, 2003. Google Scholar
  16. T. Kotek and J. A. Makowsky. Connection matrices and the definability of graph parameters. Logical Methods in Computer Science, 10(4), 2014. Google Scholar
  17. T. Kotek, M. Simkus, H. Veith, and F. Zuleger. Extending ALCQIO with trees. In Logic in Computer Science LICS, pages 511-522, 2015. Google Scholar
  18. L. Lovász. Large networks and graph limits, volume 60. AMS, 2012. Google Scholar
  19. P. Madhusudan, P. S. Thiagarajan, and Shaofa Yang. The MSO theory of connectedly communicating processes. In FSTTCS, pages 201-212, 2005. Google Scholar
  20. J.A. Makowsky. Algorithmic uses of the Feferman-Vaught theorem. Annals of Pure and Applied Logic, 126(1):159-213, 2004. Google Scholar
  21. G. Nelson and D.C. Oppen. Simplification by cooperating decision procedures. TOPLAS, 1(2):245-257, 1979. Google Scholar
  22. A. Pnueli. The temporal logic of programs. In FOCS, pages 46-57. IEEE, 1977. Google Scholar
  23. I. Pratt-Hartmann. Complexity of the two-variable fragment with counting quantifiers. Journal of Logic, Language and Information, 14(3):369-395, 2005. Google Scholar
  24. A.J.A. Robinson and A. Voronkov. Handbook of automated reasoning. Elsevier, 2001. Google Scholar
  25. D. Seese. The structure of the models of decidable monadic theories of graphs. Annals of pure and applied logic, 53(2):169-195, 1991. Google Scholar
  26. W. Thomas. Languages, automata, and logic. Springer, 1997. Google Scholar
  27. M.Y. Vardi. Why is modal logic so robustly decidable? Descriptive complexity and finite models, 31:149-184, 1996. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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