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.
Další formáty:   BibTeX LaTeX RIS
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
Originální 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 0302-9743
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
Změnil Změnil: prof. RNDr. Petr Hliněný, Ph.D., učo 168881. Změněno: 30. 3. 2016 10:02.
Anotace
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 VaVNá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 MUNá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 MUNá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
VytisknoutZobrazeno: 24. 7. 2024 00:18