偏序集上的快速概率FO模型检验
Faster Existential FO Model Checking on Posets
摘要：
证明了偏序集上一阶逻辑存在片段的模型检验问题是关于公式和偏序集宽度（反链的最大长度）的固定参数可处理的.虽然在图上对FO模型检验有很长的研究，但最近Bova，Ganian和Szeider（CSL-LICS 2014）开始了对偏序集上这个问题的研究，他们证明了FO的存在片段对于固定宽度的偏序集具有FPT算法。我们从两个方面改进了他们的结果：（1）我们的算法的运行时间是O（f（|ϕ| n（n）= n（n），n（n）= n（n），n（n）= n（n），n（n）= n（|ϕ|). n^{h（w）}），（2）我们的证明更简单，更容易理解。我们补充这一结果表明，在一定的复杂性理论假设下，存在的FO模型检验问题没有一个多项式内核。
英文摘要：
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(|ϕ|,w).n^2) on n-element posets of width w, compared to O(g(|ϕ|). 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
