Model Checking Existential Logic on Partially Ordered Sets

Result code in 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>

Result on the web

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

Result language

angličtina

Original language name

Model Checking Existential Logic on Partially Ordered Sets

Original language description

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.

Czech name

—

Czech description

—

Type

J_imp - Article in a specialist periodical, which is included in the Web of Science database

CEP classification

—

OECD FORD branch

10200 - Computer and information sciences

Project

—

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2016

Confidentiality

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

Name of the periodical

ACM Trans. Comput. Log.

ISSN

1529-3785

e-ISSN

—

Volume of the periodical

17

Issue of the periodical within the volume

2

Country of publishing house

US - UNITED STATES

Number of pages

35

Pages from-to

1-35

UT code for WoS article

000373902700003

EID of the result in the Scopus database

2-s2.0-84948988989