DI Martin Korp  
Home Teaching Research
Research
Publications Talks TTT2 TTTbox

Termination Analysis by Tree Automata Completion

In the following we report on the experiments we performed with TTT2 and CaT on version 7.2 of the TPDB All tests were performed on a server equipped with eight dual-core AMD Opteron™ 885 processors running at a clock rate of 2.6 GHz on 64 GB of system memory. For all experiments we used a 60 seconds time limit. We remark that similar results have been obtained on a dual-core laptop.

Match-Bounds

Below we report on the experiments we performed with TTT2 using the match-bound technique. As testbed we considered the 1370 TRSs of the TPDB that fulfill the variable condition. In the first part of the experiments we deal with non-left-linear systems (155 TRSs in total) and test for e-raise-boundedness, both with the explicit approach for handling raise rules described in the first paragraph of Subsection 4.4.2 and the implicit approach using raise-consistent tree automata. To simplify the representation we use the abbreviations t, r, and m to indicate that we test for top-, roof-, and match-raise-boundedness. The usage of right-hand sides of forward closures is indicated by rfc. In the second part of the experiments we deal e(-raise)-DP-bounds. Besides the recursive SCC algorithm and the improved estimated dependency graph processor, we use the following four DP processors:
s The subterm criterion.
p Polynomial orderings with 0/1 coefficients.
b The DP processor of Theorem 5.2 for left-linear DP problems and the DP processor of Theorem 5.14 for non-left-linear DP problems.
d The DP processor of Corollary 5.12 for left-linear TRSs and the one of Corollary 5.20 for non-left-linear TRSs.
For the latter two, if the DP problem is non-duplicating we take e = match. For duplicating problems we take e = roof for b and e = top for d. The usage of usable rules is indicated by ur.

Experimental Results:

Dependency Graphs

Below we report on the experiments we performed with TTT2 on the 1370 TRSs of the full termination category and the 358 TRSs of the innermost of the TPDB that fulfill the variable condition.
Full Termination
Besides the recursive SCC algorithm and linear polynomial orderings with 0/1 coefficients we use the following DP processors:
t A simple and fast approximation of the dependency graph processor of Definition 5.31 using root comparisons to estimate the dependency graph.
e The dependency graph processor with the estimation DGe(P,R) of Definition 5.50.
s The dependency graph processor with the estimation DGs(P,R) described in Section 5.3.4.
nv The dependency graph processor with the estimation DGnv(P,R) described in Section 5.3.4.
g The dependency graph processor with the estimation DGg(P,R) described in Section 5.3.4.
c The dependency graph processor with DGc(P,R) of Definition 5.37.
r The improved dependency graph processor of Theorem 5.45 with IDGc(P,R) of Definition 5.47 for right-linear P U R and DGc(P,R) for non-right-linear P U R.
* The composition of t, e, c and r with a time limit of 500 milliseconds each for the latter three.
Experimental Results:
Innermost Termination
Besides the recursive SCC algorithm and linear polynomial orderings with 0/1 coefficients we use the following DP processors:
t A simple and fast approximation of the innermost dependency graph processor defined in Definition 5.56 using root comparisons to estimate the innermost dependency graph.
e The innermost dependency graph processor with the estimation DGei(P,R) of Definition 5.64.
c The innermost dependency graph processor with DGci(P,R) of Definition 5.62.
r The improved innermost dependency graph processor of Theorem 5.60 with IDGci(P,R) of Definition 5.62 for right-linear P U R and DGci(P,R) for non-right-linear P U R.
* The composition of t, e, c, and r with a time limit of 500 milliseconds each for the latter three.
Experimental Results:

Complexity Analysis

In the following we report on the experiments we performed with CaT on the 1172 TRSs in the complexity category fo the TPDB that are non-duplicating. To compute upper complexity bounds we used the following techniques:
b The ordinary match-bound technique described in Theorems 4.4 and 4.15. To estimate the derivational complexity of a TRS we have chosen as initial language the set of all ground terms and to evaluate the runtime complexity of a TRS we considered the set of all constructor-based terms.
p The CP processor based on strongly linear interpretations with 0/1 coefficients.
m Two CP processors based on triangular matrix interpretations of dimension two and three with 0/1 coefficients.
r The CP processors of Theorems 6.23 and 6.24. Similar as for ordinary match-bounds we considered as initial language the set of all ground terms to estimate the derivational complexity of a TRS and the set of all constructor-based terms to evaluate the runtime complexity of a TRS.
Experimental Results: