TcT 2.0 on Runtime Complexity Examples

This test illustrates the gain in power when using the decompose, dependency pairs and dependency graph decomposition processors.

Testbed

As testbed we used the runtime complexity examples from the TcT source distribution. This generated testbed can be downloaded from here. We assess both the runtime complexity (columns RC below) and innermost runtime complexity (columns IRC below) of these TRSs here.

Setup

All experiments were performed on a machine with 8 dual core AMD Opteron(tm) 885 processors @ 2.60GHz processors and 16Gb of RAM. The experiments were generated using following TcT configuration resulting in this x86_64 binary. Employed strategies are recorded in the test file.

Applied Techniques

On these pages we contrast following techniques:

• semantic methods:
  With this test we check the power of semantical methods employed directly on the input TRS, which clearly illustrates the need for transformations. As processors we used matrix interpretations of dimension one to four, as well as polynomial interpretations, run in parallel.
• DP + decompose:
  In this test we indicate the strength of Zankl and Korps modular approach as described in Modular Complexity Analysis via Relative Complexity, in a dependency pair setting. We first apply the weak dependency pair (in case the weightgap condition can be established), respectively dependency tuples transformation. As central processor we then use the (de)composition processor, in combination with above mentioned semantical methods. We direct the semantic methods toward orienting leafs in the dependency graph, so that these can be dropped from the dependency problem. Also, we employ various simplifications, usable rules for instance. Compare our framework paper.
  This test indicates the usefulness of the dependency pair transformations and the decomposition processor, but still a majority of the problems remain open, both for runtime and innermost runtime complexity analysis.
• DP + DG decompose:
  This test indicates the strengh of our new dependency graph decomposition processor. Here we first transform the input problem into a depenency pair problem (DP problem for short). To avoid imprecision of the certificate, we try to solve the resulting problem as in the test decompose. Only when this approach gets stuck, we decompose the dependency graph (DG for short) by separating topmost cycles from the DP problem. This procedure gets repeated until all cycles are eventually solved.
  The experimental data shows the gain in power through this modular approach, in particular for the innermost runtime complexity setting. For runtime complexity analysis with respect to full rewriting, the impact is less severe. This has to do with the fact that for full rewriting, one also has to account for duplication of redexes, which in the DP setting implies that one has to also estimate applications of usable rules which are not covered by DG decomposition.
  A clear drawback of this method however is that DG decomposition might overestimate the complexity. In order to retain a precise complexity certificate, we are forced to apply this method only as a last means, which results in signifficantly higher execution times.

Experimental Results

Overview

Average Execution Time (in seconds)

Details

Results are also available as a Prolog database.