Model Checking Existential Logic on Partially Ordered Sets

J 2016

Model Checking Existential Logic on Partially Ordered Sets

GANIAN, Robert; Stefan SZEIDER a Simone BOVA

Základní údaje

Originální název

Model Checking Existential Logic on Partially Ordered Sets

Autoři

GANIAN, Robert (203 Česká republika, garant, domácí); Stefan SZEIDER (40 Rakousko) a Simone BOVA (380 Itálie)

Vydání

ACM Trans. Comput. Log. USA, ACM, 2016, 1529-3785

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10200 1.2 Computer and information sciences

Stát vydavatele

Spojené státy

Utajení

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

Odkazy

URL

Impakt faktor

Impact factor: 0.961

Kód RIV

RIV/00216224:14330/16:00100545

Organizační jednotka

Fakulta informatiky

DOI

http://dx.doi.org/10.1145/2814937

UT WoS

000373902700003

EID Scopus

2-s2.0-84948988989

Klíčová slova anglicky

model checking; parameterized complexity; partially ordered sets; width

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 18. 5. 2018 06:47, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

We study the problem of checking whether an existential sentence (that is, a first-order sentence in prefix form built using existential quantifiers and all Boolean connectives) is true in a finite partially ordered set (in short, a poset). A poset is a reflexive, antisymmetric, and transitive digraph. The problem encompasses the fundamental embedding problem of finding an isomorphic copy of a poset as an induced substructure of another poset. Model checking existential logic is already NP-hard on a fixed poset; thus we investigate structural properties of posets yielding conditions for fixed-parameter tractability when the problem is parameterized by the sentence. We identify width as a central structural property (the width of a poset is the maximum size of a subset of pairwise incomparable elements); our main algorithmic result is that model checking existential logic on classes of finite posets of bounded width is fixed-parameter tractable. We observe a similar phenomenon in classical complexity, where we prove that the isomorphism problem is polynomial-time tractable on classes of posets of bounded width; this settles an open problem in order theory. We surround our main algorithmic result with complexity results on less restricted, natural neighboring classes of finite posets, establishing its tightness in this sense. We also relate our work with (and demonstrate its independence of) fundamental fixed-parameter tractability results for model checking on digraphs of bounded degree and bounded clique-width.

Návaznosti

MSM0021622419, záměr

Název: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy

Citovat

GANIAN, Robert; Stefan SZEIDER a Simone BOVA. Model Checking Existential Logic on Partially Ordered Sets. ACM Trans. Comput. Log. USA: ACM, 2016, roč. 17, č. 2, s. 1-35. ISSN 1529-3785. Dostupné z: https://dx.doi.org/10.1145/2814937.

@article{1414006,
   author = {Ganian, Robert and Szeider, Stefan and Bova, Simone},
   article_location = {USA},
   article_number = {2},
   doi = {http://dx.doi.org/10.1145/2814937},
   keywords = {model checking; parameterized complexity; partially ordered sets; width},
   language = {eng},
   issn = {1529-3785},
   journal = {ACM Trans. Comput. Log.},
   title = {Model Checking Existential Logic on Partially Ordered Sets},
   url = {https://dl.acm.org/citation.cfm?id=2603110},
   volume = {17},
   year = {2016}
}

TY  - JOUR
ID  - 1414006
AU  - Ganian, Robert - Szeider, Stefan - Bova, Simone
PY  - 2016
TI  - Model Checking Existential Logic on Partially Ordered Sets
JF  - ACM Trans. Comput. Log.
VL  - 17
IS  - 2
SP  - 1-35
EP  - 1-35
PB  - ACM
SN  - 15293785
KW  - model checking
KW  - parameterized complexity
KW  - partially ordered sets
KW  - width
UR  - https://dl.acm.org/citation.cfm?id=2603110
L2  - https://dl.acm.org/citation.cfm?id=2603110
N2  - We study the problem of checking whether an existential sentence (that is, a first-order sentence in prefix form built using existential quantifiers and all Boolean connectives) is true in a finite partially ordered set (in short, a poset). A poset is a reflexive, antisymmetric, and transitive digraph. The problem encompasses the fundamental embedding problem of finding an isomorphic copy of a poset as an induced substructure of another poset. Model checking existential logic is already NP-hard on a fixed poset; thus we investigate structural properties of posets yielding conditions for fixed-parameter tractability when the problem is parameterized by the sentence. We identify width as a central structural property (the width of a poset is the maximum size of a subset of pairwise incomparable elements); our main algorithmic result is that model checking existential logic on classes of finite posets of bounded width is fixed-parameter tractable. We observe a similar phenomenon in classical complexity, where we prove that the isomorphism problem is polynomial-time tractable on classes of posets of bounded width; this settles an open problem in order theory. We surround our main algorithmic result with complexity results on less restricted, natural neighboring classes of finite posets, establishing its tightness in this sense. We also relate our work with (and demonstrate its independence of) fundamental fixed-parameter tractability results for model checking on digraphs of bounded degree and bounded clique-width.
ER  -

GANIAN, Robert; Stefan SZEIDER a Simone BOVA. Model Checking Existential Logic on Partially Ordered Sets. \textit{ACM Trans. Comput. Log.}. USA: ACM, 2016, roč.~17, č.~2, s.~1-35. ISSN~1529-3785. Dostupné z: https://dx.doi.org/10.1145/2814937.

Přehled o publikaci