Główne pojęcia
The vertex integrity parameter allows for efficient model checking of First-Order (FO) and Monadic Second-Order (MSO) logic, achieving a complexity that is intermediate between the well-studied parameters of vertex cover and tree-depth.
Streszczenie
The paper investigates the algorithmic trade-offs involved with the vertex integrity parameter from the perspective of algorithmic meta-theorems for FO and MSO logic. The key findings are:
For graphs G with vertex integrity k and FO formulas ϕ with q quantifiers, deciding if G satisfies ϕ can be done in time 2^O(k^2q + q log q) + n^O(1).
For graphs G with vertex integrity k and MSO formulas ϕ with q vertex and set quantifiers, deciding if G satisfies ϕ can be done in time 2^2^O(k^2 + kq) + n^O(1).
These complexities are significantly better than the corresponding meta-theorems for tree-depth, which involve towers of exponentials, but worse than the roughly 2^O(kq) and 2^2^O(k+q) complexities known for vertex cover.
The authors show that this deterioration in complexity is unavoidable. They present formula constructions that lead to fine-grained complexity lower bounds, establishing that the quadratic dependence on k in the upper bounds is the best possible, under the Exponential Time Hypothesis (ETH). This demonstrates that vertex integrity has a complexity for FO and MSO logic which is truly intermediate between vertex cover and tree-depth.