Faster Existential FO Model Checking on Posets

Investor logo

Warning

This publication doesn't include Institute of Computer Science. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

GAJARSKÝ Jakub HLINĚNÝ Petr OBDRŽÁLEK Jan ORDYNIAK Sebastian

Year of publication 2014
Type Article in Proceedings
Conference ISAAC 2014, LNCS 8889
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-319-13075-0_35
Field Informatics
Keywords existential first-order logic; parameterized complexity; kernelization; poset embedding
Description We prove that the model checking problem for the existen- tial 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 (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 comple- ment 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:

You are running an old browser version. We recommend updating your browser to its latest version.

More info