This website contains additional information on our paper “From Innermost to Full Probabilistic Term Rewriting: Almost-Sure Termination, Complexity, and Modularity”. The conference version of our paper was published at FoSSaCS 2024 and a longer conference version including all appendices is available at arXiv.
We now wrote a revised and extended journal version of our paper, published in “Logical Methods in Computer Science”, that is also available at arXiv. We revised this website according to the new version. This website now provides information on our implementation in the tool AProVE and we describe our revised and extended experiments. Moreover, you can find the original experiments of the conference paper as well.
The easiest way to run AProVE is via its web interface (for PTRSs in WST format or in ARI format). In addition, recent releases of AProVE are available for download on GitHub. Master_2025_06_04 is the newest release that is able to analyze full almost-sure termination (fAST) by checking the conditions of our newly developed theorems and then analyzing innermost almost-sure termination (iAST). Moreover, it can analyze the expected runtime complexity (derivational complexity) using our newly developed theorems by analyzing the expected innermost runtime complexity (derivational complexity) instead. For the analysis of probabilistic term rewrite systems, the following dependencies have to be installed (see here for more installation instructions):
Extending the path environment is necessary so that AProVE can find these programs.
In the following, we first describe the input syntax of a PTRS file. Then, we explain more details about our implementation. In the end, we describe how to execute the implementation via the web interface and via the JAR file on GitHub.
Our implementation allows for multiple different input formats of PTRSs.
First, AProVE can parse the input syntax for PTRSs that was first described in the paper ADY20. Here, the PTRS file needs to have the extension .ptrs. The syntax extends the WST format for term rewrite systems by adding a new syntax for probabilistic rules. A probabilistic rewrite rule has the form:
lhs -> w1 : rhs1 || ... || wk : rhsk
Here, lhs, rhs1, …, rhsk are terms and w1, …, wk are natural numbers > 0. This corresponds to the rule:
lhs -> {w1/w : rhs1, ..., wk/w : rhsk}
where w is the sum of w1, …, wk.
This syntax does not use the actual probabilities but rather computes them after summing up all occurring numbers in a rule. Hence, we also allow the following syntax for probabilistic rules:
lhs -> a1/b1 : rhs1 || ... || ak/bk : rhsk
Here, lhs, rhs1, …, rhsk are again terms and a1, …, ak and b1, …, bk are natural numbers > 0 that describe the actual probabilities. This corresponds to the rule:
lhs -> {a1/b1 : rhs1, ..., ak/bk : rhsk}
However, one has to ensure that the value ai/bi is actually between 0 and 1, and that the sum of all probabilities in a rule is 1. Otherwise, AProVE rejects the input file with an exception. The PTRS may contain rules in both notations.
One can use AProVE to prove termination, AST, or SAST of PTRSs w.r.t. either full or innermost rewriting, and w.r.t. either arbitrary or only basic start terms.
Moreover, one can also analyze expected runtime and derivational complexity w.r.t. either full or innermost rewriting.
The proof goal can be indicated via the keywords STRATEGY, GOAL, and STARTTERM.
The input file has to contain either (GOAL TERMINATION), (GOAL AST), (GOAL SAST), or (GOAL COMPLEXITY).
If the input file contains (STRATEGY INNERMOST), then AProVE tries to prove the provided goal w.r.t. innermost evaluation, and if the file does not contain the STRATEGY keyword, then AProVE tries to prove the provided goal w.r.t. full rewriting.
This is analogous for the STARTTERM keyword: If the input file contains (STARTTERM BASIC), then AProVE tries to prove the provided goal w.r.t. basic start terms, and if the file does not contain the STARTTERM keyword, then AProVE tries to prove the provided goal w.r.t. arbitrary start terms.
Second, AProVE can also parse the new ARI format for (probabilistic) term rewrite systems from the annual termination competition. Then, the PTRS file must have the extension .ari.
As described in the input syntax section, we only allow for rational probabilities. Internally, we store probabilities as fractions, by storing the numerator and denominator as integers. However, once we need to check satisfiability of polynomial (in)equations, we multiply the (in)equations with appropriate integers so that the resulting SMT-problem only deals with natural polynomials.
Up to now, our main technique for termination analysis of PTRSs was the probabilistic DP framework (KG23, KDG24, KG24, KG25) which can handle both innermost and full rewriting. However, the DP framework for innermost rewriting is substantially more powerful. So whenever possible, it is beneficial to move from analyzing full rewriting to analyzing innermost rewriting instead. Now, if one wants to analyze fAST for basic start terms, then we first try to prove that the conditions of our new Thm. 5.9 are satisfied. If this succeeds, then we can use the DP framework in order to prove iAST, which then implies fAST. Otherwise, we use the DP framework to prove fAST, or we try to prove fAST using the direct application of polynomial orderings from KG23. For the remaining strategy to prove iAST or how to find upper bounds on the expected runtime complexity, we refer to here and here, respectively. The strategy for arbitrary start terms is completely analogous, but with Thm. 4.2 instead of Thm. 5.9.
Our implementation can be tested via a web interface (for PTRSs in WST format or in ARI format).
Enter Program Code shows the program that is currently analyzed. The user can modify the program or replace it by a new one.Upload a File of a program to analyze (where the file should have the extension .ptrs).Submit calls AProVE in order to prove almost-sure termination of the given PTRS.Return to program input takes you back to the web page with the input program.After downloading AProVE and installing all dependencies, make sure that the path variables are set as described above. Then AProVE can be run on the file rw1.ptrs by executing
java -ea -jar aprove.jar -m wst rw1.ptrs
If you want to see the full proof, you can use the option -p plain for a plain text version or -p html for an HTML format.
java -ea -jar aprove.jar -m wst rw1.ptrs -p plain
java -ea -jar aprove.jar -m wst rw1.ptrs -p html
For the journal version of our paper, we performed new experiments in order to compare our results to the first DP framework for fAST which we developed in KG24. For this evaluation, we used the set of 130 benchmarks that was used in the evaluation of KG24. The full set of all 130 benchmarks can be downloaded here.
In the following table, we compare AProVE’s results for basic start terms when using the new theorems to switch from proving fAST to iAST (Thm. 4.2 (Thm. 17 in the conference paper) and Thm. 5.9 (previously Thm. 33)). Furthermore, we show the results for a version of AProVE (called old in the tables below) that uses the direct application of polynomials of KG23 and the DP framework of KG24 for proving fAST, and the new version of AProVE (called new in the tables below) that combines Thm. 4.2, Thm. 5.9, and the DP framework of KG24.
We tested AProVE on an M4 Macbook Pro with 16 GB of memory and used a timeout of 60 seconds for each example.
The following table shows the overall results for basic start terms.
| Examples | old (Basic) | old + Thm 4.2 (Basic) | new (Basic) |
|---|---|---|---|
| 130 | 59 | 65 | 70 |
We also give a table to show the overall results for arbitrary start terms.
| Examples | old | new |
|---|---|---|
| 130 | 52 | 57 |
Note that AProVE can prove innermost AST for 109 of the 130 examples. The result and output of AProVE for each individual run can be downloaded here. The CSVs containing the results are here: old, old (Basic), old + Thm 4.2 (Basic), new, and new (Basic).
The following experimental results should be interpreted with caution. We have identified an error in the proofs of Thm. 27 and Thm. 38, which affects the soundness of the corresponding processors in general. We are currently investigating whether a slightly adjusted version of the processor is nevertheless sound.
To evaluate the power of our approach for our conference paper at FoSSaCS 2024, we used the set of 100 benchmarks from here and added 18 new examples (including the 11 examples from the paper).
The full set of benchmarks can be downloaded here, where the subdirectory FoSSaCS24 contains our 18 new examples.
For a detailed explanation of every single new benchmark see below.
In the following table, we compare AProVE’s results for basic start terms when using the different new theorems to switch from proving fAST to iAST (Thm. 17, Thm. 27, Thm. 33, Thm. 38). Note that Thm. 33 subsumes Thm. 17 and Thm. 38 subsumes Thm. 27 for basic start terms, since right-linearity implies spareness. Furthermore, we show the results for the old version of AProVE that only uses the direct application of polynomials of KG23 for proving fAST, and the new version of AProVE that combines Thm. 33 and Thm. 38, as described above.
We tested AProVE using StarExec, which provides an Intel Xeon E5-2609 CPU with 2.4 GHz and 264 GB of RAM.
Here, the result YES indicates a successful fAST proof, and
the result MAYBE indicates that the tool crashed or terminated the verification process within the given time without a result.
The result NO indicates a successful fAST disproof, however this can only occur if the PTRS only contains trivial probabilities and is non-terminating, as we did not implement any specific technique to disprove fAST yet.
As in the Termination Competition, a timeout of 300 seconds was used for each example.
The following table shows the overall results for basic start terms.
| Examples | old AProVE | Thm. 17 | Thm. 27 | Thm. 33 | Thm. 38 | new AProVE |
|---|---|---|---|---|---|---|
| 118 | 36 | 48 | 44 | 58 | 56 | 61 |
From the 58 examples that we can solve by using both Thm. 33 and Thm. 38 in ``new AProVE’’, 5 examples (that are all right-linear) can only be solved by Thm. 33, 3 examples (where one is right-linear and the others only spare) can only be solved by Thm. 38, and 50 can be solved by both. Furthermore, AProVE can prove iAST for 90 of the 115 examples.
A detailed table with the result for each individual benchmark can be downloaded here.
Finally, we also give a table to show the overall results for arbitrary start terms.
| Examples | old AProVE | Thm. 17 | Thm. 27 | new AProVE |
|---|---|---|---|---|
| 118 | 36 | 48 | 44 | 49 |