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)
- 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)
- M
- max/plus interpretations of the form fA(x1,....,xn) = max{b0, a1(x1 + b1), ..., an(x1 + bn)} with ai in {0,1} and bi in N
- L
- lexicographic path orders (LPO) with argument filtering
- Wd
- weighted path orders (WPO) with algebras based on ed
- 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. On the other hand, A ⊆ WA holds. Column A-B in the following table tries AA, BB, AB, and (then) BA Here AB stands for the lexicographic combination of A and B. 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 L, LL, LLL, Ed, S2,S2S2, S2S2S2, E1L, LE1, and E1E1 amounts to 50, which is covered by LL ∪ E4.
- 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 | LE1 | M | MM | WM | WE1 | WE2 | WS2 | WM-WE2 | WM-WS2 | WE2-WS2 | AProVE | NaTT | total |
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
YES | 57 | 4 | 20 | 22 | 8 | 43 | 45 | 47 | 10 | 47 | 47 | 41 | 30 | 27 | 6 | 12 | 20 | 29 | 47 | 31 | 48 | 48 | 47 | 86 | 66 | 106 |
(sec) | 0.80 | 0.22 | 3.40 | 5.08 | 0.57 | 5.03 | 9.72 | 27.05 | 1.11 | 16.90 | 27.20 | 4.03 | 4.81 | 3.97 | 0.30 | 0.68 | 3.02 | 12.13 | 27.82 | 27.69 | 60.45 | 74.81 | 56.61 | 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 | 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 | 0.00 | 34.36 | 0.80 | |
MAYBE | 0 | 122 | 106 | 104 | 118 | 83 | 81 | 79 | 116 | 79 | 79 | 85 | 96 | 99 | 120 | 114 | 106 | 97 | 79 | 95 | 78 | 78 | 79 | 0 | 53 | 123 |
(sec) | 0.00 | 4.28 | 5.63 | 7.10 | 3.15 | 2.16 | 3.95 | 7.27 | 4.32 | 5.27 | 8.82 | 2.06 | 3.00 | 3.08 | 3.44 | 3.88 | 6.68 | 5.06 | 7.58 | 10.56 | 30.47 | 40.40 | 38.93 | 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 | 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 | 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 | 126 |