Treewidth in verification: Local vs. global

The treewidth of a graph measures how close the graph is to a tree. Many problems that are intractable for general graphs, are tractable when the graph has bounded treewidth. Recent works study the complexity of model checking for state transition systems of bounded treewidth. There is little reason to believe, however, that the treewidth of the state transition graphs of real systems, which we refer to as global treewidth, is bounded. In contrast, we consider in this paper concurrent transition systems, where communication between concurrent components is modeled explicitly. Assuming boundedness of the treewidth of the communication graph, which we refer to as local treewidth, is reasonable, since the topology of communication in concurrent systems is often constrained physically. In this work we study the impact of local treewidth boundedness on the complexity of verification problems. We first present a positive result, proving that a CNF formula of bounded treewidth can be represented by an OBDD of polynomial size. We show, however, that the nice properties of treewidth-bounded CNF formulas are not preserved under existential quantification or unrolling. Finally, we show that the complexity of various verification problems is high even under the assumption of local treewidth boundedness. In summary, while global treewidth boundedness does have computational advantages, it is not a realistic assumption; in contrast, local treewidth boundedness is a realistic assumption, but its computational advantages are rather meager.