Experiments on relative termination problems
General Information
Our termination tool employs the dependency pair method by Iborra et al. (2017) with cycle analysis of dependency graphs, reduction pairs, and rule removal by monotone reduction pairs. Note that usable rules are not used due to a soundness reason. The problem set is taken from the TRS Relative category of the Termination Problem Database.
- d
- applicability of the dependency pair method by Iborra et al. (2017)
(R dominates S and S is non-duplicating)
- L
- lexicographic path orders (LPO) with argument filtering
- Ed
- echelon-form matrix interpretations on Nd with 0,1-matrix coefficients, equipped with the lexicographic order (Section 5)
- Sd
- matrix interpretations on Nd with 0,1-matrix coefficients, equipped with the standard order (by Endrullis et al. 2008)
- AProVE
- AProVE 2024
- NaTT
- NaTT (termCOMP 2022 version)
For instance, E1L stands for the lexicographic combination of E1 and L. Note that E1 and S1 are identical. Concerning heterogeneous combinations, (e.g.) E1 ⊆ E1L does not hold in general, as weak orientation by E1 does not guarantee weak orientation by L. Concerning NaTT, we employed the termCOMP 2022 version, which is the latest correct version among available versions for relative termination proofs.
Y: YES | proved termination |
---|---|
N: NO | proved non-termination |
M: MAYBE | failed to prove |
T: TIMEOUT | exceeded time limit 60 seconds |
E: ERROR | tool terminated with some error |
Note
- The 57 problems where d is labeled YES are the targets of our experiments.
- L ⊆ LL ⊆ LLL.
- E1 ⊆ E1E1 ⊆ E2 ⊆ E3 ⊆ E4.
- S2 ⊆ S2S2 ⊆ S2S2S2.
- On the 57 problems the union of all methods except AProVE and NaTT amounts to 50.
- The 50 problems includes 11 problems that AProVE missed.
- The 50 problems includes 5 problems that NaTT missed.
status | d | L | LL | LLL | E1 | E2 | E3 | E4 | S2 | S2S2 | S2S2S2 | E1E1 | E1L | E2L | E3L | E4L | LE1 | LE2 | LE3 | LE4 | E2S2 | S2E2 | AProVE | NaTT | total |
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
YES | 57 | 4 | 20 | 22 | 8 | 43 | 45 | 47 | 10 | 47 | 47 | 41 | 30 | 47 | 47 | 49 | 27 | 31 | 31 | 31 | 47 | 45 | 86 | 66 | 106 |
(sec) | 0.80 | 0.21 | 4.01 | 6.36 | 0.54 | 5.00 | 10.27 | 29.09 | 1.13 | 17.75 | 28.86 | 3.83 | 5.11 | 11.23 | 22.90 | 59.86 | 4.47 | 6.72 | 14.11 | 26.34 | 13.05 | 13.30 | 111.90 | 7.58 | |
NO | 69 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 13 | 5 | 71 |
(sec) | 0.97 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 34.36 | 0.80 | |
MAYBE | 0 | 122 | 106 | 104 | 118 | 83 | 81 | 79 | 116 | 79 | 79 | 85 | 96 | 79 | 79 | 77 | 99 | 95 | 95 | 95 | 79 | 81 | 0 | 53 | 122 |
(sec) | 0.00 | 4.68 | 6.53 | 9.12 | 2.88 | 2.18 | 4.07 | 7.64 | 4.43 | 5.56 | 9.15 | 1.98 | 3.15 | 3.43 | 7.17 | 9.22 | 3.23 | 3.86 | 6.94 | 12.22 | 4.04 | 5.22 | 0.00 | 72.39 | |
TIMEOUT | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 27 | 2 | 27 |
(sec) | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 1620.00 | 120.00 | |
total | 126 | 126 | 126 | 126 | 126 | 126 | 126 | 126 | 126 | 126 | 126 | 126 | 126 | 126 | 126 | 126 | 126 | 126 | 126 | 126 | 126 | 126 | 126 | 126 |