Model Checking Existential Logic on Partially Ordered Sets

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F16%3A00100545" target="_blank" >RIV/00216224:14330/16:00100545 - isvavai.cz</a>

Výsledek na webu

<a href="https://dl.acm.org/citation.cfm?id=2603110" target="_blank" >https://dl.acm.org/citation.cfm?id=2603110</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1145/2814937" target="_blank" >10.1145/2814937</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Model Checking Existential Logic on Partially Ordered Sets

Popis výsledku v původním jazyce

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ázev v anglickém jazyce

Model Checking Existential Logic on Partially Ordered Sets

Popis výsledku anglicky

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.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10200 - Computer and information sciences

Projekt

—

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2016

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

ACM Trans. Comput. Log.

ISSN

1529-3785

e-ISSN

—

Svazek periodika

17

Číslo periodika v rámci svazku

2

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

35

Strana od-do

1-35

Kód UT WoS článku

000373902700003

EID výsledku v databázi Scopus

2-s2.0-84948988989