First-Order Logic with Connectivity Operators: expressiveness and model-checking
First-order logic (\(FO\)) can express many algorithmic problems on graphs, such as the independent set and dominating set problem parameterized by solution size. On the other hand, \(FO\) cannot express the very simple algorithmic question whether two vertices are connected. We enrich \(FO\) with connectivity predicates that are tailored to express algorithmic graph properties that are commonly studied in parameterized algorithmics. By adding the atomic predicates \(conn_k(x,y,z_1,\ldots, z_k)\)that hold true in a graph if there exists a path between (the valuations of) \(x\) and \(y\) after (the valuations of) \(z_1,\ldots, z_k\) have been deleted, we obtain separator logic. We thereby obtain a logic that can express many interesting problems such as the feedback vertex set problem and elimination distance problems to first-order definable classes.
We first study the expressive power of the new logic. We then study the model-checking problem and prove that from the point of view of parameterized complexity, under standard complexity theoretical assumptions, the frontier of tractability of separator logic is almost exactly delimited by classes excluding a fixed topological minor. From the atomic case of connectivity predicates we obtain the first deterministic data structure for connectivity under batched vertex failures where for every fixed number of failures, all operations can be performed in constant time.