Model checking existential logic on partially ordered sets

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

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

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
• scientific article; zbMATH DE number 1688350
• 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

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

• Linear time solvable optimization problems on graphs of bounded clique-width
• Upper bounds to the clique width of graphs
• Graph structure and monadic second-order logic. A language-theoretic approach
• The Computational Structure of Monotone Monadic SNP and Constraint Satisfaction: A Study through Datalog and Group Theory
• Color-coding
• Closure properties of constraints
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The isomorphism problem for varieties generated by a two-element algebra

Cited In (13)

• 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
• Faster existential FO model checking on posets
• FO model checking of geometric graphs
• 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
• Faster existential FO model checking on posets
• Chain minors are FPT
• Model checking existential logic on partially ordered sets
• The Model Checking Problem for Prefix Classes of Second-Order Logic: A Survey

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)