Faster Existential FO Model Checking on Posets

J 2015

Faster Existential FO Model Checking on Posets

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

Basic information

Original name

Faster Existential FO Model Checking on Posets

Authors

GAJARSKÝ, Jakub (703 Slovakia, guarantor, belonging to the institution), Petr HLINĚNÝ (203 Czech Republic, belonging to the institution), Jan OBDRŽÁLEK (203 Czech Republic, belonging to the institution) and Sebastian ORDYNIAK (276 Germany, belonging to the institution)

Edition

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

Other information

Language

English

Type of outcome

Článek v odborném periodiku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

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

References:

URL

Impact factor

Impact factor: 0.569

RIV identification code

RIV/00216224:14330/15:00081186

Organization unit

Faculty of Informatics

DOI

http://dx.doi.org/10.2168/LMCS-11(4:8)2015

UT WoS

000373922900008

Keywords in English

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

Abstract

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.

Links

GA14-03501S, research and development project

Name: Parametrizované algoritmy a kernelizace v kontextu diskrétní matematiky a logiky

Investor: Czech Science Foundation

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

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

Investor: Masaryk University, Category A

Citovat

GAJARSKÝ, Jakub, Petr HLINĚNÝ, Jan OBDRŽÁLEK and Sebastian ORDYNIAK. Faster Existential FO Model Checking on Posets. Logical Methods in Computer Science. Německo: Logical Methods in Computer Science e.V., 2015, vol. 11, No 4, p. 1-13. ISSN 1860-5974. Available from: https://dx.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 = {http://dx.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 and 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, vol.~11, No~4, p.~1-13. ISSN~1860-5974. Available from: https://dx.doi.org/10.2168/LMCS-11(4:8)2015.

Detailed Information on Publication Record