Working Seminar on Formal Models, Discrete Structures, and Algorithms

The Model Checking Problem on Partially Ordered Sets

Robert Ganian (TU Wien)

When: April 28, 2:00pm

Where: room G2.91b/G215


We provide a parameterized and classical complexity overview of the problem of checking whether a logical sentence is true in a finite partially ordered set (in short, a poset). Model checking on arbitrary posets is intractable even for sentences from very simple logics, and so we turn our attention to fundamental structural invariants of posets and ask whether these allow for efficient model checking of richer logics. The fundamental poset invariants we consider here are width, depth, degree and cover-degree.

Since posets can be defined as reflexive, antisymmetric and transitive digraphs, it is possible to apply a number of well-established graph-theoretic model checking frameworks such as Courcelle’s theorems and Seese’s algorithm. However, with respect to the considered invariants, these frameworks can only be applied to posets of bounded degree. We obtain complexity bounds for posets of bounded depth and cover-degree; in particular, we show that already Existential FO logic and Conjunctive Positive FO logic are W[1]-hard on such posets (while Existential Conjunctive Positive FO logic is trivially tractable on any poset). On the other hand, we show that model checking for these two fragments of FO logic is fixed parameter tractable on posets of bounded width.