Gajarský, Jakub and Hliněný, Petr and Obdržálek, Jan and Ordyniak, Sebastian - Faster Existential FO Model Checking on Posets

lmcs:1609 - Logical Methods in Computer Science, December 11, 2015, Volume 11, Issue 4
Faster Existential FO Model Checking on Posets

Authors: Gajarský, Jakub and Hliněný, Petr and Obdržálek, Jan and Ordyniak, Sebastian

We prove that the model checking problem for the existential fragment of first-order (FO) logic on partially ordered sets is fixed-parameter tractable (FPT) with respect to the formula and the width of a poset (the maximum size of an antichain). While there is a long line of research into FO model checking on graphs, the study of this problem on posets has been initiated just recently by Bova, Ganian and Szeider (CSL-LICS 2014), who proved that the existential fragment of FO has an FPT algorithm for a poset of fixed width. We improve upon their result in two ways: (1) the runtime of our algorithm is O(f(|{\phi}|,w).n^2) on n-element posets of width w, compared to O(g(|{\phi}|). n^{h(w)}) of Bova et al., and (2) our proofs are simpler and easier to follow. We complement this result by showing that, under a certain complexity-theoretical assumption, the existential FO model checking problem does not have a polynomial kernel.


Source : oai:arXiv.org:1409.4433
DOI : 10.2168/LMCS-11(4:8)2015
Volume: Volume 11, Issue 4
Published on: December 11, 2015
Submitted on: January 6, 2015
Keywords: Computer Science - Logic in Computer Science,Computer Science - Discrete Mathematics


Share

Consultation statistics

This page has been seen 112 times.
This article's PDF has been downloaded 25 times.