Easy instances for model checking

Our interest is focused on the complexity of the model-checking problem and its generalizations. This question is intimately related to the expressibility of the logical language in question. We investigate the parameterized complexity of queries expressible in monadic second order logic over tree-like structures (structures with bounded tree-width) and first order logic over locally tree-like structures. The importance of the latter stems from the fact that structures of bounded valence, planar graphs and graphs with bounded crossing number are all locally tree-like. And thus our results apply to these classes. <br> <br>For each of these two questions we consider the following questions: (i) decide, if a query hold in a structure (ii) compute an assignment that make a query true in a structure (iii) compute all satisfying assignments and (iv) compute the number of satisfying assignments. <br> <br>We give algorithms that solve these questions in optimal time, i.e. in time linear in the size of the structure (+ the output, if there is noteworthy output). In particular, we show that counting the number of dominating set of size k can be done in linear time on planar graphs.

Author dc:creator

• Frick, Markus

Contributors dc:contributor

• Grohe, Martin

• parameterized complexity
• treewidth
• algorithms
• logic

Repository record source_url

https://freidok.uni-freiburg.de/data/229

OAI identifier oai:identifier

oai:freidok.uni-freiburg.de:229