Document Open Access Logo

Reducing CMSO Model Checking to Highly Connected Graphs

Authors Daniel Lokshtanov, M. S. Ramanujan, Saket Saurabh, Meirav Zehavi

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2018.135.pdf
  • Filesize: 0.52 MB
  • 14 pages

Document Identifiers

Author Details

Daniel Lokshtanov
  • University of Bergen, Norway
M. S. Ramanujan
  • University of Warwick, United Kingdom
Saket Saurabh
  • The Institute of Mathematical Sciences, HBNI, Chennai, India
Meirav Zehavi
  • Ben-Gurion University, Israel

Funding

  • Lokshtanov, Daniel: Supported by \emph{Pareto-Optimal Parameterized Algorithms}, ERC Starting Grant 715744
  • Ramanujan, M. S.: Supported by \emph{BeHard}, Bergen Research Foundation and \emph{X-Tract}, Austrian Science Fund (FWF, project P26696)
  • Saurabh, Saket: Supported by \emph{Parameterized Approximation}, ERC Starting Grant 306992.

Cite As Get BibTex

Daniel Lokshtanov, M. S. Ramanujan, Saket Saurabh, and Meirav Zehavi. Reducing CMSO Model Checking to Highly Connected Graphs. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 135:1-135:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.ICALP.2018.135

Abstract

Given a Counting Monadic Second Order (CMSO) sentence psi, the CMSO[psi] problem is defined as follows. The input to CMSO[psi] is a graph G, and the objective is to determine whether G |= psi. Our main theorem states that for every CMSO sentence psi, if CMSO[psi] is solvable in polynomial time on "globally highly connected graphs", then CMSO[psi] is solvable in polynomial time (on general graphs). We demonstrate the utility of our theorem in the design of parameterized algorithms. Specifically we show that technical problem-specific ingredients of a powerful method for designing parameterized algorithms, recursive understanding, can be replaced by a black-box invocation of our main theorem. We also show that our theorem can be easily deployed to show fixed parameterized tractability of a wide range of problems, where the input is a graph G and the task is to find a connected induced subgraph of G such that "few" vertices in this subgraph have neighbors outside the subgraph, and additionally the subgraph has a CMSO-definable property.

Subject Classification

ACM Subject Classification
  • Theory of computation → Fixed parameter tractability
Keywords
  • Fixed Parameter Tractability Model Checking Recursive Understanding

Metrics

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

Related Versions

References

  1. Karl Abrahamson and Michael Fellows. Finite automata, bounded treewidth and well-quasiordering. In Graph structure theory (Seattle, WA, 1991), volume 147 of Contemp. Math., pages 539-563, Providence, RI, 1993. Amer. Math. Soc. URL: http://dx.doi.org/10.1090/conm/147/01199.
  2. Stefan Arnborg, Jens Lagergren, and Detlef Seese. Easy problems for tree-decomposable graphs. Journal of Algorithms, 12:308-340, 1991. Google Scholar
  3. Hans L. Bodlaender, Fedor V. Fomin, Daniel Lokshtanov, Eelko Penninkx, Saket Saurabh, and Dimitrios M. Thilikos. (Meta) kernelization. J. ACM, 63(5):44:1-44:69, 2016. URL: http://dl.acm.org/citation.cfm?id=2973749, URL: http://dx.doi.org/10.1145/2973749.
  4. Richard B. Borie, R. Gary Parker, and Craig A. Tovey. Automatic generation of linear-time algorithms from predicate calculus descriptions of problems on recursively constructed graph families. Algorithmica, 7:555-581, 1992. Google Scholar
  5. Simone Bova, Robert Ganian, and Stefan Szeider. Model checking existential logic on partially ordered sets. ACM Trans. Comput. Log., 17(2):10:1-10:35, 2016. URL: http://dx.doi.org/10.1145/2814937.
  6. Rajesh Chitnis, Marek Cygan, MohammadTaghi Hajiaghayi, Marcin Pilipczuk, and Michal Pilipczuk. Designing FPT algorithms for cut problems using randomized contractions. SIAM J. Comput., 45(4):1171-1229, 2016. URL: http://dx.doi.org/10.1137/15M1032077.
  7. B. Courcelle. The monadic second-order logic of graphs. III. Tree-decompositions, minors and complexity issues. RAIRO Inform. Théor. Appl., 26(3):257-286, 1992. Google Scholar
  8. Bruno Courcelle. The monadic second-order logic of graphs I: Recognizable sets of finite graphs. Inform. and Comput., 85:12-75, 1990. Google Scholar
  9. Bruno Courcelle. The expression of graph properties and graph transformations in monadic second-order logic. In Handbook of graph grammars and computing by graph transformation, Vol. 1, pages 313-400. World Sci. Publ, River Edge, NJ, 1997. Google Scholar
  10. Bruno Courcelle and Joost Engelfriet. Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach. Cambridge University Press, 2012. Google Scholar
  11. Marek Cygan, Fedor V. Fomin, Lukasz Kowalik, Daniel Lokshtanov, Dániel Marx, Marcin Pilipczuk, Michal Pilipczuk, and Saket Saurabh. Parameterized Algorithms. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-21275-3.
  12. A. Dawar, M. Grohe, and S. Kreutzer. Locally excluding a minor. In LICS'07, pages 270-279. IEEE Computer Society, 2007. Google Scholar
  13. Erik D. Demaine, Fedor V. Fomin, Mohammad Taghi Hajiaghayi, and Dimitrios M. Thilikos. Subexponential parameterized algorithms on bounded-genus graphs and H-minor-free graphs. J. ACM, 52(6):866-893, 2005. Google Scholar
  14. Rodney G. Downey and Michael R. Fellows. Parameterized Complexity. Springer, Berlin, 1998. Google Scholar
  15. Rodney G. Downey and Michael R. Fellows. Fundamentals of Parameterized Complexity. Texts in Computer Science. Springer, 2013. Google Scholar
  16. Zdenek Dvorak, Daniel Král, and Robin Thomas. Testing first-order properties for subclasses of sparse graphs. J. ACM, 60(5):36:1-36:24, 2013. URL: http://dx.doi.org/10.1145/2499483.
  17. Michael R. Fellows and Michael A. Langston. An analogue of the Myhill-Nerode theorem and its use in computing finite-basis characterizations (extended abstract). In Proceedings of the 30th Annual Symposium on Foundations of Computer Science (FOCS 1989), pages 520-525. IEEE, 1989. Google Scholar
  18. J. Flum and M. Grohe. Fixed-parameter tractability, definability, and model-checking. SIAM J. Comput., 31(1):113-145, 2001. Google Scholar
  19. M. Frick and M. Grohe. Deciding first-order properties of locally tree-decomposable structures. J. ACM, 48(6):1184-1206, 2001. Google Scholar
  20. Jakub Gajarský, Petr Hlinený, Jan Obdrzálek, and Sebastian Ordyniak. Faster existential FO model checking on posets. Logical Methods in Computer Science, 11(4), 2015. URL: http://dx.doi.org/10.2168/LMCS-11(4:8)2015.
  21. Robert Ganian, Petr Hlinený, Daniel Král, Jan Obdrzálek, Jarett Schwartz, and Jakub Teska. FO model checking of interval graphs. Logical Methods in Computer Science, 11(4), 2015. URL: http://dx.doi.org/10.2168/LMCS-11(4:11)2015.
  22. Martin Grohe, Ken-ichi Kawarabayashi, Dániel Marx, and Paul Wollan. Finding topological subgraphs is fixed-parameter tractable. In Proceedings of the 43rd ACM Symposium on Theory of Computing, STOC 2011, San Jose, CA, USA, 6-8 June 2011, pages 479-488, 2011. URL: http://dx.doi.org/10.1145/1993636.1993700.
  23. Martin Grohe, Stephan Kreutzer, and Sebastian Siebertz. Deciding first-order properties of nowhere dense graphs. J. ACM, 64(3):17:1-17:32, 2017. URL: http://dx.doi.org/10.1145/3051095.
  24. Ken-ichi Kawarabayashi and Mikkel Thorup. The minimum k-way cut of bounded size is fixed-parameter tractable. In IEEE 52nd Annual Symposium on Foundations of Computer Science, FOCS 2011, Palm Springs, CA, USA, October 22-25, 2011, pages 160-169, 2011. URL: http://dx.doi.org/10.1109/FOCS.2011.53.
  25. Eun Jung Kim, Christophe Paul, Ignasi Sau, and Dimitrios M. Thilikos. Parameterized algorithms for min-max multiway cut and list digraph homomorphism. J. Comput. Syst. Sci., 86:191-206, 2017. URL: http://dx.doi.org/10.1016/j.jcss.2017.01.003.
  26. Ashutosh Rai and M. S. Ramanujan. Strong parameterized deletion: Bipartite graphs. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016, December 13-15, 2016, Chennai, India, pages 21:1-21:14, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2016.21.
  27. Ashutosh Rai, M. S. Ramanujan, and Saket Saurabh. A parameterized algorithm for mixed-cut. In LATIN 2016: Theoretical Informatics - 12th Latin American Symposium, Ensenada, Mexico, April 11-15, 2016, Proceedings, pages 672-685, 2016. URL: http://dx.doi.org/10.1007/978-3-662-49529-2_50.
  28. D. Seese. Linear time computable problems and first-order descriptions. Math. Structures Comput. Sci., 6(6):505-526, 1996. 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