Faster Existential FO Model Checking on Posets

J 2015

Faster Existential FO Model Checking on Posets

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

Základní údaje

Originální název

Faster Existential FO Model Checking on Posets

Autoři

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

Vydání

Logical Methods in Computer Science, Německo, Logical Methods in Computer Science e.V. 2015, 1860-5974

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Odkazy

URL

Impakt faktor

Impact factor: 0.569

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/15:00081186

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

rst-order logic; partially ordered sets; model checking; parameterized complexity

Štítky

formela-journal

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 14. 2. 2017 09:05, prof. RNDr. Petr Hliněný, Ph.D.

Anotace

V originále

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.

Návaznosti

GA14-03501S, projekt VaV

Název: Parametrizované algoritmy a kernelizace v kontextu diskrétní matematiky a logiky

Investor: Grantová agentura ČR, Parametrizované algoritmy a kernelizace v kontextu diskrétní matematiky a logiky

MUNI/A/1159/2014, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV.

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

GAJARSKÝ, Jakub; Petr HLINĚNÝ; Jan OBDRŽÁLEK a Sebastian ORDYNIAK. Faster Existential FO Model Checking on Posets. Logical Methods in Computer Science. Německo: Logical Methods in Computer Science e.V., 2015, roč. 11, č. 4, s. 1-13. ISSN 1860-5974. Dostupné z: https://doi.org/10.2168/LMCS-11(4:8)2015.

@article{1316744,
   author = {Gajarský, Jakub and Hliněný, Petr and Obdržálek, Jan and Ordyniak, Sebastian},
   article_location = {Německo},
   article_number = {4},
   doi = {https://doi.org/10.2168/LMCS-11(4:8)2015},
   keywords = {rst-order logic; partially ordered sets; model checking; parameterized complexity},
   language = {eng},
   issn = {1860-5974},
   journal = {Logical Methods in Computer Science},
   title = {Faster Existential FO Model Checking on Posets},
   url = {http://arxiv.org/pdf/1409.4433.pdf},
   volume = {11},
   year = {2015}
}

TY  - JOUR
ID  - 1316744
AU  - Gajarský, Jakub - Hliněný, Petr - Obdržálek, Jan - Ordyniak, Sebastian
PY  - 2015
TI  - Faster Existential FO Model Checking on Posets
JF  - Logical Methods in Computer Science
VL  - 11
IS  - 4
SP  - 1-13
EP  - 1-13
PB  - Logical Methods in Computer Science e.V.
SN  - 18605974
KW  - rst-order logic
KW  - partially ordered sets
KW  - model checking
KW  - parameterized complexity
UR  - http://arxiv.org/pdf/1409.4433.pdf
N2  - 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.
ER  -

GAJARSKÝ, Jakub; Petr HLINĚNÝ; Jan OBDRŽÁLEK a Sebastian ORDYNIAK. Faster Existential FO Model Checking on Posets. \textit{Logical Methods in Computer Science}. Německo: Logical Methods in Computer Science e.V., 2015, roč.~11, č.~4, s.~1-13. ISSN~1860-5974. Dostupné z: https://doi.org/10.2168/LMCS-11(4:8)2015.

Přehled o publikaci