DAG-width of Control Flow Graphs with Applications to Model Checking

TL;DR

This paper demonstrates that control flow graphs from structured programs have bounded DAG-width, enabling efficient model checking for parity games and the mu-calculus.

Contribution

It establishes that such control flow graphs have DAG-width at most three and provides a linear time algorithm for DAG decomposition.

Findings

DAG-width of control flow graphs is at most three.

Parity games can be solved efficiently on these graphs.

Linear time algorithm for DAG decomposition is provided.

Abstract

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 $\mu$-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.