Courcelle's Theorem Made Dynamic

TL;DR

This paper demonstrates that model checking a fixed monadic second-order formula over evolving subgraphs of bounded tree-width can be efficiently maintained dynamically within DynFO, using a reduction to Dyck reachability.

Contribution

It introduces a dynamic complexity result for MSO model checking on evolving graphs with bounded tree-width, employing a novel reduction to Dyck reachability.

Findings

Model checking MSO formulas is in DynFO for bounded tree-width graphs.

The problem reduces to Dyck reachability on an acyclic automaton.

Efficient dynamic updates are possible with LOGSPACE precomputation.

Abstract

Dynamic complexity is concerned with updating the output of a problem when the input is slightly changed. We study the dynamic complexity of model checking a fixed monadic second-order formula over evolving subgraphs of a fixed maximal graph having bounded tree-width; here the subgraph evolves by losing or gaining edges (from the maximal graph). We show that this problem is in DynFO (with LOGSPACE precomputation), via a reduction to a Dyck reachability problem on an acyclic automaton.