FO Model Checking on Posets of Bounded Width

D 2015

FO Model Checking on Posets of Bounded Width

GAJARSKÝ, Jakub, Petr HLINĚNÝ, Jan OBDRŽÁLEK, Sebastian ORDYNIAK, M.S. RAMANUJAN et. al.

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

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

United States of America

Confidentiality degree

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

Publication form

electronic version available online

References:

sborník

RIV identification code

RIV/00216224:14330/15:00081183

Organization unit

Faculty of Informatics

ISBN

978-1-4673-8191-8

ISSN

DOI

http://dx.doi.org/10.1109/FOCS.2015.63

UT WoS

000379204700054

Keywords in English

model checking; first-order logic; posets; width; metatheorem

Abstract

V originále

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 project

Name: Parametrizované algoritmy a kernelizace v kontextu diskrétní matematiky a logiky

Investor: Czech Science Foundation

MUNI/A/1159/2014, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV.

Investor: Masaryk University, Category A

MUNI/A/1206/2014, interní kód MU

Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)

Investor: Masaryk University, Category A

Citovat

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. Online. In Venkatesan Guruswami. 56th Annual Symposium on Foundations of Computer Science, FOCS 2015. Berkeley, CA, USA: IEEE Computer Society, 2015, p. 963-974. ISBN 978-1-4673-8191-8. Available from: https://dx.doi.org/10.1109/FOCS.2015.63.

@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 and 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, p.~963-974. ISBN~978-1-4673-8191-8. Available from: https://dx.doi.org/10.1109/FOCS.2015.63.

Detailed Information on Publication Record