Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{1316736, author = {Gajarský, Jakub and Hliněný, Petr and Obdržálek, Jan and Ordyniak, Sebastian and Ramanujan, M.S. and Lokshtanov, Daniel and Saurabh, Saket}, address = {Berkeley, CA, USA}, booktitle = {56th Annual Symposium on Foundations of Computer Science, FOCS 2015}, doi = {http://dx.doi.org/10.1109/FOCS.2015.63}, editor = {Venkatesan Guruswami}, keywords = {model checking; first-order logic; posets; width; metatheorem}, howpublished = {elektronická verze "online"}, language = {eng}, location = {Berkeley, CA, USA}, isbn = {978-1-4673-8191-8}, pages = {963-974}, publisher = {IEEE Computer Society}, title = {FO Model Checking on Posets of Bounded Width}, url = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=7352273}, year = {2015} }
TY - JOUR ID - 1316736 AU - Gajarský, Jakub - Hliněný, Petr - Obdržálek, Jan - Ordyniak, Sebastian - Ramanujan, M.S. - Lokshtanov, Daniel - Saurabh, Saket PY - 2015 TI - FO Model Checking on Posets of Bounded Width PB - IEEE Computer Society CY - Berkeley, CA, USA SN - 9781467381918 KW - model checking KW - first-order logic KW - posets KW - width KW - metatheorem UR - http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=7352273 L2 - http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=7352273 N2 - 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. ER -
GAJARSKÝ, Jakub, Petr HLINĚNÝ, Jan OBDRŽÁLEK, Sebastian ORDYNIAK, M.S. RAMANUJAN, Daniel LOKSHTANOV a Saket SAURABH. FO Model Checking on Posets of Bounded Width. Online. In Venkatesan Guruswami. \textit{56th Annual Symposium on Foundations of Computer Science, FOCS 2015}. Berkeley, CA, USA: IEEE Computer Society, 2015, s.~963-974. ISBN~978-1-4673-8191-8. Dostupné z: https://dx.doi.org/10.1109/FOCS.2015.63.
|