一句话：证明 MSO 可定义的有界特殊树宽系统语言恰为多上下文无关语言，并用于计算向下闭包。
多下推自动机（MPDA）或交错 Dyck 可达性可建模递归程序静态分析，但一般不可判定。文献常用有界树宽给出可判定下近似，即 MSO 可定义的有界树宽系统，然而其执行动作语言仍缺乏理解。本文针对稍有不同但等价于 MPDA 上有界树宽、并涵盖已有系统的有界特殊树宽（bounded-stw），建立其与计算语言学中多上下文无关语言（MCFL）的联系，证明 MSO 可定义 bounded-stw 系统的字语言恰好是 MCFL。基于该刻画，作者给出计算向下闭包的最优算法，并展示在可动态生成 bounded-stw 进程的程序中，安全性验证与顺序递归进程具有相同复杂度。
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 multithreaded 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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2512-01973,
title = {Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures},
author = {C. Aiswarya and Pascal Baumann and Prakash Saivasan and Lia Schütze and Georg Zetzsche},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776716}
}