Monadic Second Order Finite Satisfiability and Unbounded Tree-Width
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.
Monadic Second Order Logic MSO
Two variable Fragment with Counting C2
Finite decidability
Unbounded Tree-width
WS1S with Cardinality Constraints
13:1-13:20
Regular Paper
Tomer
Kotek
Tomer Kotek
Helmut
Veith
Helmut Veith
Florian
Zuleger
Florian Zuleger
10.4230/LIPIcs.CSL.2016.13
S. Arnborg, J. Lagergren, and D. Seese. Easy problems for tree-decomposable graphs. Journal of Algorithms, 12(2):308-340, 1991.
F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, and P. F. Patel-Schneider, editors. The Description Logic handbook. Cambridge University Press, 2003.
D. Calvanese, T. Kotek, M. Šimkus, H. Veith, and F. Zuleger. Shape and content. In Integrated Formal Methods, pages 3-17. Springer, 2014.
W. Charatonik and P. Witkowski. Two-variable logic with counting and trees. In LICS, pages 73-82. IEEE, 2013.
B. Courcelle. The monadic second-order logic of graphs. i. recognizable sets of finite graphs. Information and computation, 85(1):12-75, 1990.
B. Courcelle and J. Engelfriet. Graph structure and monadic second-order logic: a language-theoretic approach, volume 138. Cambridge University Press, 2012.
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.
J. Flum and M. Grohe. Parameterized Complexity Theory. Texts in Theoretical Computer Science. Springer, 2006.
E. Grädel. On the restraining power of guards. The Journal of Symbolic Logic, 64(04):1719-1742, 1999.
E. Grädel and M. Otto. On logics with two variables. Theoretical computer science, 224(1):73-113, 1999.
E. Grädel, M. Otto, and E. Rosen. Two-variable logic with counting is decidable. In LICS, pages 306-317. IEEE, 1997.
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.
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.
W. Hodges. Model theory. In Encyclopedia of Mathematics and its Applications, volume 42. Cambridge University Press, 1993.
F. Klaedtke and H. Rueß. Monadic second-order logics with cardinalities. In Automata, Languages and Programming, pages 681-696. Springer, 2003.
T. Kotek and J. A. Makowsky. Connection matrices and the definability of graph parameters. Logical Methods in Computer Science, 10(4), 2014.
T. Kotek, M. Simkus, H. Veith, and F. Zuleger. Extending ALCQIO with trees. In Logic in Computer Science LICS, pages 511-522, 2015.
L. Lovász. Large networks and graph limits, volume 60. AMS, 2012.
P. Madhusudan, P. S. Thiagarajan, and Shaofa Yang. The MSO theory of connectedly communicating processes. In FSTTCS, pages 201-212, 2005.
J.A. Makowsky. Algorithmic uses of the Feferman-Vaught theorem. Annals of Pure and Applied Logic, 126(1):159-213, 2004.
G. Nelson and D.C. Oppen. Simplification by cooperating decision procedures. TOPLAS, 1(2):245-257, 1979.
A. Pnueli. The temporal logic of programs. In FOCS, pages 46-57. IEEE, 1977.
I. Pratt-Hartmann. Complexity of the two-variable fragment with counting quantifiers. Journal of Logic, Language and Information, 14(3):369-395, 2005.
A.J.A. Robinson and A. Voronkov. Handbook of automated reasoning. Elsevier, 2001.
D. Seese. The structure of the models of decidable monadic theories of graphs. Annals of pure and applied logic, 53(2):169-195, 1991.
W. Thomas. Languages, automata, and logic. Springer, 1997.
M.Y. Vardi. Why is modal logic so robustly decidable? Descriptive complexity and finite models, 31:149-184, 1996.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode