%0 Journal Article
%T DAG-width of Control Flow Graphs with Applications to Model Checking
%A Therese Biedl
%A Sebastian Fischmeister
%A Neeraj Kumar
%J Computer Science
%D 2015
%I arXiv
%X 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.
%U http://arxiv.org/abs/1503.00793v1