Faster Existential FO Model Checking on Posets

GAJARSKÝ, Jakub, Petr HLINĚNÝ, Jan OBDRŽÁLEK a Sebastian ORDYNIAK. Faster Existential FO Model Checking on Posets. In Hee-Kap Ahn, Chan-Su Shin. ISAAC 2014, LNCS 8889. Berlin: Springer International Publishing, 2014, s. 441-451. ISBN 978-3-319-13074-3. Dostupné z: https://dx.doi.org/10.1007/978-3-319-13075-0_35.

Základní údaje

Originální název

Faster Existential FO Model Checking on Posets

Autoři

GAJARSKÝ, Jakub (703 Slovensko, domácí), Petr HLINĚNÝ (203 Česká republika, garant, domácí), Jan OBDRŽÁLEK (203 Česká republika, domácí) a Sebastian ORDYNIAK (276 Německo, domácí)

Vydání

Berlin, ISAAC 2014, LNCS 8889, od s. 441-451, 11 s. 2014

Nakladatel

Springer International Publishing

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

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

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/14:00074016

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-13074-3

ISSN

DOI

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

UT WoS

000354865900035

Klíčová slova anglicky

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

Štítky

core_A, firank_A, formela-conference

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

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.

---

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/0765/2013, interní kód MU	Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU) Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0855/2013, interní kód MU	Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Akronym: FI MAV III.) Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty