DAG-width of Control Flow Graphs with Applications to Model Checking
This work addresses the need for efficient model checking in software verification by providing a tighter bound and algorithm for control flow graphs, though it is incremental as it builds on known treewidth results.
The paper tackled the problem of measuring the complexity of control flow graphs from structured programs by introducing DAG-width, showing it is at most three, and provided a linear-time algorithm for decomposition, enabling efficient parity games and μ-calculus model checking.
The treewidth of control flow graphs arising from structured programs is known to be at most six. However, as a control flow graph is inherently directed, it makes sense to consider a measure of width for digraphs instead. We use the so-called DAG-width and show that the DAG-width of control flow graphs arising from structured (goto-free) programs is at most three. Additionally, we also give a linear time algorithm to compute the DAG decomposition of these control flow graphs. One consequence of this result is that parity games (and hence the $μ$-calculus model checking problem), which are known to be tractable on graphs of bounded DAG-width, can be solved efficiently in practice on control flow graphs.