Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures

The reachability problem in multi-pushdown automata (MPDA), or equivalently, interleaved Dyck reachability, has many applications in static analysis of recursive programs. An example is safety verification of multi-threaded recursive programs with shared memory. Since these problems are undecidable, the literature contains many decidable (and efficient) underapproximations of MPDA. A uniform framework that captures many of these underapproximations is that of bounded treewidth : To each execution of the MPDA, we associate a graph; then we consider the subset of all graphs that have a treewidth at most k , for some constant k . In fact, bounding treewidth is a generic approach to obtain classes of systems with decidable reachability, even beyond MPDA underapproximations. The resulting systems are also called MSO-definable bounded-treewidth systems . While bounded treewidth is a powerful tool for reachability and similar types of analysis, the word languages (i.e. action sequences corresponding to executions) of these systems remain far from understood. For the slight restriction of bounded special treewidth , or “bounded-stw” (which is equivalent to bounded treewidth on MPDA, and even includes all bounded-treewidth systems studied in the literature), this work reveals a connection with multiple context-free languages (MCFL), a concept from computational linguistics. We show that the word languages of MSO-definable bounded-stw systems are exactly the MCFL. We exploit this connection to provide an optimal algorithm for computing downward closures for MSO-definable bounded-stw systems. Computing downward closures is a notoriously difficult task that has many applications in the verification of complex systems: As an example application, we show that in programs with dynamic spawning of MSO-definable bounded-stw processes, safety verification has the same complexity as in the case of processes with sequential recursive processes.