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 \emph{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 \emph{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 \emph{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 \emph{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.