Publications in Scientific Journals:
S. Bova, R. Ganian, S. Szeider:
"Model Checking Existential Logic on Partially Ordered Sets";
ACM Transactions on Computational Logic,
We study the problem of checking whether an existential sentence (i.e., a first-order sentence in prefix
form built using existential quantifiers and all Boolean connectives) is true in a finite partially ordered
set (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
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, in which we prove that the isomorphism problem is polynomialtime
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.
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
Electronic version of the publication:
Created from the Publication Database of the Vienna University of Technology.