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.

Základní údaje

Originální název

FO Model Checking on Posets of Bounded Width

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í), Sebastian ORDYNIAK (276 Německo, domácí), M.S. RAMANUJAN (356 Indie), Daniel LOKSHTANOV (578 Norsko) a Saket SAURABH (356 Indie)

Vydání

Berkeley, CA, USA, 56th Annual Symposium on Foundations of Computer Science, FOCS 2015, od s. 963-974, 12 s. 2015

Nakladatel

IEEE Computer Society

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

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

Forma vydání

elektronická verze "online"

Odkazy

sborník

Kód RIV

RIV/00216224:14330/15:00081183

Organizační jednotka

Fakulta informatiky

ISBN

978-1-4673-8191-8

ISSN

DOI

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

UT WoS

000379204700054

Klíčová slova anglicky

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

Štítky

core_A, firank_1, formela-conference

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 27. 8. 2019 11:58, RNDr. Pavel Šmerk, Ph.D.

Anotace

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.

Návaznosti

GA14-03501S, projekt VaV

Ná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 MU

Ná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

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

Ná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

Citovat

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. 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.

@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.

Podrobný výpis o publikaci