Graph-theoretic Properties of Control Flow Graphs and Applications

This thesis deals with determining appropriate width parameters of control flow graphs so that certain computationally hard problems of practical interest become efficiently solvable. A well-known result of Thorup states that the treewidth of control flow graphs arising from structured (goto-free) programs is at most six. However, since a control flow graph is inherently directed, it is very likely that using a digraph width measure would give better algorithms for problems where directional properties of edges are important. One such problem, parity game, is closely related to the μ-calculus model checking problem in software verification and is known to be tractable on graphs of bounded DAG-width, Kelly-width or entanglement. Motivated by this, we show that the DAG-width of control flow graphs arising from structured programs is at most three and give a linear-time algorithm to compute the corresponding DAG decomposition. Using similar techniques, we show that Kelly-width of control flow graphs is also bounded by three. Additionally, we also show that control flow graphs can have unbounded entanglement. In light of these results, we revisit the complexity of the μ-calculus model checking problem on these special graph classes and show that we can obtain better running times for control flow graphs