Faster existential FO model checking on posets

DOI10.1007/978-3-319-13075-0_35MaRDI QIDQ5892117zbMATH OpenOpenAlexFDO

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

Publication date 11 September 2015

Published in Algorithms and Computation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1409.4433

Mathematics Subject Classification ID

Parameterized complexity, tractability and kernelization (68Q27) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: 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.

Recommendations

• Faster existential FO model checking on posets
• Quantified conjunctive queries on partially ordered sets
• Quantified conjunctive queries on partially ordered sets

Cites work

• Advice classes of parametrized tractability
• Closure properties of constraints
• Faster existential FO model checking on posets
• scientific article; zbMATH DE number 2234775 (Why is no real title available?)
• Kernelization: new upper and lower bound techniques
• On problems without polynomial kernels
• Parametrized complexity theory.
• Recognition algorithms for orders of small width and graphs of small Dilworth number
• Solving MAX-\(r\)-SAT above a tight lower bound

Cited in

(7)

• FO model checking on geometric graphs
• Quantified conjunctive queries on partially ordered sets
• Quantified conjunctive queries on partially ordered sets
• Twin-width. I: Tractable FO model checking
• FO model checking of geometric graphs
• Faster existential FO model checking on posets
• Faster existential FO model checking on posets

This page was built for publication: Faster existential FO model checking on posets

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5892117)