Complexity, Graphs, and the Dependency Pair Method

This paper builds on recent efforts (Hirokawa and Moser, 2008) to exploit the dependency pair method for verifying feasible, i.e., polynomial runtime complexities of term rewrite systems automatically. We extend our earlier results by revisiting dependency graphs in the context of complexity analysis. The obtained new results are easy to implement and considerably extend the analytic power of our existing methods. The gain in power is even more significant when compared to existing methods that directly, i.e., without the use of transformations, induce feasible runtime complexities. We provide ample numerical data for assessing the viability of the method.Proceedings of the 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008