[Back]


Talks and Poster Presentations (with Proceedings-Entry):

S. Bova, R. Ganian, St. Szeider:
"Model Checking Existential Logic on Partially Ordered Sets";
Talk: Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Vienna; 2014-07-14 - 2014-07-18; in: "CSL-LICS 2014", ACM New York, NY, USA, (2014), ISBN: 978-1-4503-2886-9.



English abstract:
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 fixedparameter
tractability results for model checking on digraphs of
bounded degree and bounded clique-width.


Related Projects:
Project Head Stefan Szeider:
Exploiting New Types of Structure for Fixed Parameter Tractability

Project Head Stefan Szeider:
Parameterized Compilation

Project Head Stefan Szeider:
The Parameterized Complexity of Reasoning Problems


Created from the Publication Database of the Vienna University of Technology.