Document Open Access Logo

Current Trends and New Perspectives for First-Order Model Checking (Invited Talk)

Author Stephan Kreutzer

PDF
Thumbnail PDF

File

LIPIcs.CSL.2017.4.pdf
  • Filesize: 356 kB
  • 5 pages

Document Identifiers

Author Details

Stephan Kreutzer

Cite AsGet BibTex

Stephan Kreutzer. Current Trends and New Perspectives for First-Order Model Checking (Invited Talk). In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 4:1-4:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CSL.2017.4

Abstract

The model-checking problem for a logic LLL is the problem of decidig for a given formula phi in LLL and structure AA whether the formula is true in the structure, i.e. whether AA models phi. Model-checking for logics such as First-Order Logic (FO) or Monadic Second-Order Logic (MSO) has been studied intensively in the literature, especially in the context of algorithmic meta-theorems within the framework of parameterized complexity. However, in the past the focus of this line of research was model-checking on classes of sparse graphs, e.g. planar graphs, graph classes excluding a minor or classes which are nowhere dense. By now, the complexity of first-order model-checking on sparse classes of graphs is completely understood. Hence, current research now focusses mainly on classes of dense graphs. In this talk we will briefly review the known results on sparse classes of graphs and explain the complete classification of classes of sparse graphs on which first-order model-checking is tractable. In the second part we will then focus on recent and ongoing research analysing the complexity of first-order model-checking on classes of dense graphs.
Keywords
  • Finite Model Theory
  • Computational Model Theory
  • Algorithmic Meta Theorems
  • Model-Checking
  • Logical Approaches in Graph Theory

Metrics

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

References

  1. 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.
  2. B. Courcelle. Graph rewriting: An algebraic and logic approach. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume 2, pages 194-242. Elsevier, 1990. Google Scholar
  3. Bruno Courcelle, Janos Makowsky, and Udi Rotics. Linear time solvable optimization problems on graphs of bounded clique-width. Theory of Computing Systems, 33(2):125-150, 2000. Google Scholar
  4. A. Dawar, M. Grohe, and S. Kreutzer. Locally excluding a minor. In Logic in Computer Science (LICS), pages 270-279, 2007. Google Scholar
  5. Zdeněk Dvořák, Daniel Král, and Robin Thomas. Deciding first-order properties for sparse graphs. In 51st Annual IEEE Symposium on Foundations of Computer Science (FOCS), 2010. Google Scholar
  6. Jörg Flum, Markus Frick, and Martin Grohe. Query evaluation via tree-decompositions. J. ACM, 49(6):716-752, 2002. URL: http://dx.doi.org/10.1145/602220.602222.
  7. Jörg Flum and Martin Grohe. Fixed-parameter tractability, definability, and model checking. SIAM Journal on Computing, 31:113-145, 2001. Google Scholar
  8. Jakub Gajarský, Petr Hlinený, Daniel Lokshtanov, Jan Obdrzálek, Sebastian Ordyniak, M. S. Ramanujan, and Saket Saurabh. FO model checking on posets of bounded width. In IEEE 56th Annual Symposium on Foundations of Computer Science, FOCS 2015, Berkeley, CA, USA, 17-20 October, 2015, pages 963-974, 2015. URL: http://dx.doi.org/10.1109/FOCS.2015.63.
  9. Jakub Gajarský, Petr Hlinený, Jan Obdrzálek, Daniel Lokshtanov, and M. S. Ramanujan. A new perspective on FO model checking of dense graph classes. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'16, New York, NY, USA, July 5-8, 2016, pages 176-184, 2016. URL: http://dx.doi.org/10.1145/2933575.2935314.
  10. 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.
  11. Martin Grohe and Stephan Kreutzer. Methods for algorithmic meta-theorems. Contemporary Mathematics, 588, American Mathematical Society 2011. Google Scholar
  12. Martin Grohe, Stephan Kreutzer, and Sebastian Siebertz. Deciding first-order properties of nowhere dense graphs. In 46th Annual Symposium on the Theory of Computing (STOC), 2014. Google Scholar
  13. Stephan Kreutzer, Roman Rabinovich, and Sebastian Siebertz. Polynomial kernels and wideness properties of nowhere dense graph classes. In Proceedings of the Twenty-Eighth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2017, Barcelona, Spain, Hotel Porta Fira, January 16-19, pages 1533-1545, 2017. URL: http://dx.doi.org/10.1137/1.9781611974782.100.
  14. Stephan Kreutzer and Siamak Tazari. Lower bounds for the complexity of monadic second-order logic. In Logic in Computer Science (LICS), 2010. Google Scholar
  15. Stephan Kreutzer and Siamak Tazari. On brambles, grid-like minors, and parameterized intractability of monadic second-order logic. In Symposium on Discrete Algorithms (SODA), 2010. Google Scholar
  16. Alexander Langer, Felix Reidl, Peter Rossmanith, and Somnath Sikdar. Evaluation of an mso-solver. In Algorithm Engineering &Experiments (ALENEX), pages 55-63, 2012. Google Scholar
  17. Jaroslav Nešetřil and Patrice Ossona de Mendez. Sparsity. Springer, 2012. Google Scholar
  18. Jaroslav Nešetřil and Patrice Ossona de Mendez. First order properties of nowhere dense structures. Journal of Symbolic Logic, 75(3):868-887, 2010. Google Scholar
  19. Jaroslav Nešetřil and Patrice Ossona de Mendez. On nowhere dense graphs. European Journal of Combinatorics, 32(4):600-617, 2011. Google Scholar
  20. Detlev Seese. Linear time computable problems and first-order descriptions. Mathematical Structures in Computer Science, 5:505-526, 1996. Google Scholar
  21. Luc Segoufin and Alexandre Vigny. Constant Delay Enumeration for FO Queries over Databases with Local Bounded Expansion. In Michael Benedikt and Giorgio Orsi, editors, 20th International Conference on Database Theory (ICDT 2017), volume 68 of Leibniz International Proceedings in Informatics (LIPIcs), pages 20:1-20:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.ICDT.2017.20.
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 Imprint Privacy Contact