Faster Existential FO Model Checking on Posets
| Authors | |
|---|---|
| Year of publication | 2015 |
| Type | Article in Periodical |
| Magazine / Source | Logical Methods in Computer Science |
| MU Faculty or unit | |
| Citation | |
| Web | http://arxiv.org/pdf/1409.4433.pdf |
| Doi | http://dx.doi.org/10.2168/LMCS-11(4:8)2015 |
| Field | Informatics |
| Keywords | rst-order logic; partially ordered sets; model checking; parameterized complexity |
| Description | 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)*n2) 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. |
| Related projects: |