Automated Complexity Analysis Based on the Dependency Pair Method

Nao Hirokawa and Georg Moser

Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR 2008), Lecture Notes in Artificial Intelligence 5195, pp. 364 – 380, 2008.


In this paper, we present a variant of the dependency pair method for analysing runtime complexities of term rewrite systems automatically. This method is easy to implement, but significantly extends the analytic power of existing direct methods. Our findings extend the class of TRSs whose linear or quadratic runtime complexity can be detected automatically. We provide ample numerical data for assessing the viability of the method.


Unfortunately the conference paper contains a bug. As stated Theorem 23 is not valid as the condition that TRS S is non-duplicating is missing. The mistake happens in the seemingly trivial Lemma 22, where also non-duplication of S needs to be assumed. We are grateful to Dieter Hofbauer and Andreas Schnabl who compiled a counter-example that shows the need for the additional restriction. Consider the TRSs R = { f(s(x),y) → f(x,d(y,y,y) }
and S = { d(0,0,x) → x, d(s(x),s(y),z) → d(x,y,s(z)) }. Then Theorem 23 would be applicable and wrongly concludes linear runtime complexity for the combined system, while the combined system actually has at least exponential runtime complexity. By introducing the assumption ‘non-duplication of S’ the results in Section 5 can be re-established.

  PDF |    doi:10.1007/978-3-540-71070-7_32  |  © Springer


author = "Nao Hirokawa and Georg Moser",
title = "Automated Complexity Analysis Based on the Dependency Pair Method",
booktitle = "Proceedings of the 4th International Joint Conference on Automated Reasoning",
series = "Lecture Notes in Artificial Intelligence",
volume = 5195,
pages = "364--380",
publisher = "Springer-Verlag",
year = 2008

Nach oben scrollen