D 2014

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, belonging to the institution), Petr HLINĚNÝ (203 Czech Republic, guarantor, belonging to the institution), Jan OBDRŽÁLEK (203 Czech Republic, belonging to the institution) and Sebastian ORDYNIAK (276 Germany, belonging to the institution)

Edition

Berlin, ISAAC 2014, LNCS 8889, p. 441-451, 11 pp. 2014

Publisher

Springer International Publishing

Other information

Language

English

Type of outcome

Stať ve sborníku

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í

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/14:00074016

Organization unit

Faculty of Informatics

ISBN

978-3-319-13074-3

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-13075-0_35

UT WoS

000354865900035

Keywords in English

existential first-order logic; parameterized complexity; kernelization; poset embedding

Tags

core_A, firank_A, formela-conference

Tags

International impact, Reviewed
Změněno: 30/3/2016 10:02, prof. RNDr. Petr Hliněný, Ph.D.

Abstract

V originále

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

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/0765/2013, interní kód MU
Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)
Investor: Masaryk University, Category A
MUNI/A/0855/2013, interní kód MU
Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Acronym: FI MAV III.)
Investor: Masaryk University, Category A
Displayed: 5/11/2024 07:59