Faster Existential FO Model Checking on Posets

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F14%3A00074016" target="_blank" >RIV/00216224:14330/14:00074016 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-319-13075-0_35" target="_blank" >http://dx.doi.org/10.1007/978-3-319-13075-0_35</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-13075-0_35" target="_blank" >10.1007/978-3-319-13075-0_35</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Faster Existential FO Model Checking on Posets

Popis výsledku v původním jazyce

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). Whilethere 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.

Název v anglickém jazyce

Faster Existential FO Model Checking on Posets

Popis výsledku anglicky

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). Whilethere 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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GA14-03501S" target="_blank" >GA14-03501S: Parametrizované algoritmy a kernelizace v kontextu diskrétní matematiky a logiky</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2014

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

ISAAC 2014, LNCS 8889

ISBN

9783319130743

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

11

Strana od-do

441-451

Název nakladatele

Springer International Publishing

Místo vydání

Berlin

Místo konání akce

Korea

Datum konání akce

1. 1. 2014

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—