Graph-theoretic Properties of Control Flow Graphs and Applications

treewidth;DAG-width;entanglement;Kelly-width;control flow graphs;mu-calculus model checking;special graph classes;Computer Science

Kumar, Neeraj

University of Waterloo

关键词: treewidth;    DAG-width;    entanglement;    Kelly-width;    control flow graphs;    mu-calculus model checking;    special graph classes;    Computer Science;   

Others  :  https://uwspace.uwaterloo.ca/bitstream/10012/9580/1/Kumar_Neeraj.pdf

瑞士|英语

来源: UWSPACE Waterloo Institutional Repository

【 摘 要 】

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. Onesuch 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.