Model checking existential logic on partially ordered sets

DOI10.1145/2603088.2603110zbMATH Open1401.68187arXiv1405.2891OpenAlexW2064113986WikidataQ130854254 ScholiaQ130854254MaRDI QIDQ4635604FDOQ4635604

Simone Bova, Robert Ganian, Stefan Szeider

Publication date: 23 April 2018

Published in: ACM Transactions on Computational Logic, Proceedings of the 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) (Search for Journal in Brave)

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 fixed-parameter tractability results for model checking on digraphs of bounded degree and bounded clique-width.

Full work available at URL: https://arxiv.org/abs/1405.2891

zbMATH Keywords

model checkingparameterized complexitypartially ordered setswidth

Mathematics Subject Classification ID

Partial orders, general (06A06) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Linear time solvable optimization problems on graphs of bounded clique-width
• Upper bounds to the clique width of graphs
• The Computational Structure of Monotone Monadic SNP and Constraint Satisfaction: A Study through Datalog and Group Theory
• Color-coding
• Closure properties of constraints
• Deciding First-Order Properties of Nowhere Dense Graphs
• On the dimensions of ordered sets of bounded degree
• Recognition algorithms for orders of small width and graphs of small Dilworth number
• The isomorphism problem for varieties generated by a two-element algebra

Cited In (11)

• Faster Existential FO Model Checking on Posets
• Quantified conjunctive queries on partially ordered sets
• Quantified Conjunctive Queries on Partially Ordered Sets
• FO model checking on geometric graphs
• Quantified Constraints in Twenty Seventeen
• Finding Finite Models in Multi-sorted First-Order Logic
• Reducing CMSO model checking to highly connected graphs
• A linear-time parameterized algorithm for computing the width of a DAG
• Model checking existential logic on partially ordered sets
• The Model Checking Problem for Prefix Classes of Second-Order Logic: A Survey
• Title not available (Why is that?)

   Recommendations

• Model checking existential logic on partially ordered sets 👍 👎
• Model-Checking on Ordered Structures 👍 👎
• Model Checking and Validity in Propositional and Modal Inclusion Logics 👍 👎
• Model checking and validity in propositional and modal inclusion logics 👍 👎
• Title not available (Why is that?) 👍 👎
• Model Checking for Modal Intuitionistic Dependence Logic 👍 👎
• Decidability of order-based modal logics 👍 👎
• Faster Existential FO Model Checking on Posets 👍 👎
• Faster Existential FO Model Checking on Posets 👍 👎
• Bounded Model Checking for Partial Kripke Structures 👍 👎

This page was built for publication: Model checking existential logic on partially ordered sets

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635604)