Kreutzer, Stephan
Current Trends and New Perspectives for FirstOrder Model Checking (Invited Talk)
Abstract
The modelchecking 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.
Modelchecking for logics such as FirstOrder Logic (FO) or
Monadic SecondOrder Logic (MSO) has been studied intensively
in the literature, especially in the context of algorithmic metatheorems
within the framework of parameterized complexity. However, in the past the
focus of this line of research was modelchecking 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
firstorder modelchecking 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 firstorder modelchecking is tractable.
In the second part we will then focus on recent and ongoing research
analysing the complexity of firstorder modelchecking on classes of
dense graphs.
BibTeX  Entry
@InProceedings{kreutzer:LIPIcs:2017:7709,
author = {Stephan Kreutzer},
title = {{Current Trends and New Perspectives for FirstOrder Model Checking (Invited Talk)}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {4:14:5},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770453},
ISSN = {18688969},
year = {2017},
volume = {82},
editor = {Valentin Goranko and Mads Dam},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7709},
URN = {urn:nbn:de:0030drops77095},
doi = {10.4230/LIPIcs.CSL.2017.4},
annote = {Keywords: Finite Model Theory, Computational Model Theory, Algorithmic Meta Theorems, ModelChecking, Logical Approaches in Graph Theory}
}
16.08.2017
Keywords: 

Finite Model Theory, Computational Model Theory, Algorithmic Meta Theorems, ModelChecking, Logical Approaches in Graph Theory 
Seminar: 

26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Issue date: 

2017 
Date of publication: 

16.08.2017 