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 (703 Slovensko, garant, domácí), Petr HLINĚNÝ (203 Česká republika, domácí), Jan OBDRŽÁLEK (203 Česká republika, domácí) a Sebastian ORDYNIAK (276 Německo, domácí)

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

Impakt faktor

Impact factor: 0.569

Kód RIV

RIV/00216224:14330/15:00081186

Organizační jednotka

Fakulta informatiky

DOI

UT WoS

000373922900008

Klíčová slova anglicky

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

Štítky

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