Match-Bounds Revisited
Below we report on the experiments we performed with TTT2 on the 1331 TRSs in version 5.0 of the TPDB that fulfill the variable condition. All tests were performed on a workstation equipped with an Intel® Pentium™ M processor running at a CPU rate of 2 GHz and 1 GB of system memory. For all experiments we used a 60 seconds time limit. In the first part of the experiments we deal with non-left-linear systems (158 TRSs in total) and test for e-raise-boundedness, both with the explicit approach for handling raise rules described in the first paragraph of Section 4 and the implicit approach using raise-consistent tree automata. To simplify the representation we use the abbreviationst, 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 38 for left-linear DP problems and the DP processor of Theorem 49 for non-left-linear DP problems |
d |
the DP processor of Corollary 48 for left-linear TRSs and the one of Corollary 55 for non-left-linear TRSs |
b and e = top for d. The usage of usable
rules is indicated by ur.
Experimental Results:
- e-raise-bounds:
- compatible tree automata: results and statistics
- quasi-compatible tree automata: results and statistics
- e(-raise)-DP-bounds:
- compatible tree automata: results and statistics
- quasi-compatible tree automata: results and statistics