GAJARSKÝ, Jakub, Petr HLINĚNÝ, Jan OBDRŽÁLEK a Sebastian ORDYNIAK. Faster Existential FO Model Checking on Posets. Logical Methods in Computer Science. Německo: Logical Methods in Computer Science e.V., 2015, roč. 11, č. 4, s. 1-13. ISSN 1860-5974. Dostupné z: https://dx.doi.org/10.2168/LMCS-11(4:8)2015.
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, 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
Originální 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í
WWW URL
Impakt faktor Impact factor: 0.569
Kód RIV RIV/00216224:14330/15:00081186
Organizační jednotka Fakulta informatiky
Doi http://dx.doi.org/10.2168/LMCS-11(4:8)2015
UT WoS 000373922900008
Klíčová slova anglicky rst-order logic; partially ordered sets; model checking; parameterized complexity
Štítky formela-journal
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: 14. 2. 2017 09:05.
Anotace
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 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/1159/2014, interní kód MUNá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
VytisknoutZobrazeno: 25. 4. 2024 04:23