License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2017.4
URN: urn:nbn:de:0030-drops-77095
URL: http://drops.dagstuhl.de/opus/volltexte/2017/7709/
Go to the corresponding LIPIcs Volume Portal


Kreutzer, Stephan

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

pdf-format:
LIPIcs-CSL-2017-4.pdf (0.3 MB)


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.

BibTeX - Entry

@InProceedings{kreutzer:LIPIcs:2017:7709,
  author =	{Stephan Kreutzer},
  title =	{{Current Trends and New Perspectives for First-Order Model Checking (Invited Talk)}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{4:1--4:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Valentin Goranko and Mads Dam},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7709},
  URN =		{urn:nbn:de:0030-drops-77095},
  doi =		{10.4230/LIPIcs.CSL.2017.4},
  annote =	{Keywords: Finite Model Theory, Computational Model Theory, Algorithmic Meta Theorems, Model-Checking, Logical Approaches in Graph Theory}
}

Keywords: Finite Model Theory, Computational Model Theory, Algorithmic Meta Theorems, Model-Checking, Logical Approaches in Graph Theory
Seminar: 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Issue Date: 2017
Date of publication: 14.08.2017


DROPS-Home | Fulltext Search | Imprint Published by LZI