GAJARSKÝ, Jakub, Petr HLINĚNÝ, Jan OBDRŽÁLEK, Sebastian ORDYNIAK, M.S. RAMANUJAN, Daniel LOKSHTANOV and Saket SAURABH. FO Model Checking on Posets of Bounded Width. In Venkatesan Guruswami. 56th Annual Symposium on Foundations of Computer Science, FOCS 2015. Berkeley, CA, USA: IEEE Computer Society. p. 963-974. ISBN 978-1-4673-8191-8. doi:10.1109/FOCS.2015.63. 2015.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name FO Model Checking on Posets of Bounded Width
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), Sebastian ORDYNIAK (276 Germany, belonging to the institution), M.S. RAMANUJAN (356 India), Daniel LOKSHTANOV (578 Norway) and Saket SAURABH (356 India).
Edition Berkeley, CA, USA, 56th Annual Symposium on Foundations of Computer Science, FOCS 2015, p. 963-974, 12 pp. 2015.
Publisher IEEE Computer Society
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher United States of America
Confidentiality degree is not subject to a state or trade secret
Publication form electronic version available online
WWW sborník
RIV identification code RIV/00216224:14330/15:00081183
Organization unit Faculty of Informatics
ISBN 978-1-4673-8191-8
ISSN 0272-5428
Doi http://dx.doi.org/10.1109/FOCS.2015.63
UT WoS 000379204700054
Keywords in English model checking; first-order logic; posets; width; metatheorem
Tags core_A, firank_1, formela-conference
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 27/8/2019 11:58.
Abstract
Over the past two decades the main focus of research into first-order (FO) model checking algorithms have been sparse relational structures-culminating in the FPT-algorithm by Grohe, Kreutzer and Siebertz for FO model checking of nowhere dense classes of graphs [STOC'14], with dense structures starting to attract attention only recently. Bova, Ganian and Szeider [LICS'14] initiated the study of the complexity of FO model checking on partially ordered sets (posets). Bova, Ganian and Szeider showed that model checking existential FO logic is fixed-parameter tractable (FPT) on posets of bounded width, where the width of a poset is the size of the largest antichain in the poset. The existence of an FPT algorithm for general FO model checking on posets of bounded width, however, remained open. We resolve this question in the positive by giving an algorithm that takes as its input an n-element poset P of width w and an FO logic formula and determines whether the formula holds on the poset in FPT quadratic time with respect to both the width of the poset and size of the formula.
Links
GA14-03501S, research and development projectName: Parametrizované algoritmy a kernelizace v kontextu diskrétní matematiky a logiky
Investor: Czech Science Foundation
MUNI/A/1159/2014, interní kód MUName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV.
Investor: Masaryk University, Category A
MUNI/A/1206/2014, interní kód MUName: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)
Investor: Masaryk University, Category A
PrintDisplayed: 28/3/2024 19:53