eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-08-16
4:1
4:5
10.4230/LIPIcs.CSL.2017.4
article
Current Trends and New Perspectives for First-Order Model Checking (Invited Talk)
Kreutzer, Stephan
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol082-csl2017/LIPIcs.CSL.2017.4/LIPIcs.CSL.2017.4.pdf
Finite Model Theory
Computational Model Theory
Algorithmic Meta Theorems
Model-Checking
Logical Approaches in Graph Theory