This web site contains additional information on our paper “Annotated Dependency Pairs for Full Almost-Sure Termination of Probabilistic Term Rewriting”. More precisely, we provide a long version of our paper including all appendices and proofs, information on our implementation in the tool AProVE, and we describe our experiments.
The easiest way to run AProVE is via its web interface (for PTRSs in WST format or in ARI format).
Moreover, recent releases of AProVE are available for download on GitHub. Release master_2024_06_16 is able to analyze termination, almost-sure termination (AST), and positive almost-sure termination (PAST) of PTRSs w.r.t. different rewrite strategies, and implements the new ADP framework for AST w.r.t. full rewriting. For termination 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 all w1,…,wk.
Since this syntax does not use the actual probabilities but rather computes them after summing up all occurring numbers in a rule, this might be a little confusing to read. 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 PAST of PTRSs w.r.t. either full or innermost rewriting. The proof goal can be indicated via the keywords ‘STRATEGY’ and ‘GOAL’. The input file has to contain either ‘(GOAL TERMINATION)’, ‘(GOAL AST)’, or ‘(GOAL PAST)’. If the input file contains ‘(STRATEGY INNERMOST)’, then AProVE tries to prove the provided goal w.r.t. innermost evaluation for the PTRS in the input file and if the file does not contain the ‘STRATEGY’ keyword, then AProVE tries to prove the provided goal w.r.t. full rewriting.
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 (e.g., in the direct application of polynomial interpretations) we multiply the (in)equations with appropriate integers so that the resulting SMT-problem only deals with natural polynomials.
For AST, we first check whether the conditions from KFG24 are satisfied in order to switch to innermost rewriting. If this succeeds, then we can use the strategy to prove innermost AST as described here. Otherwise, we use our new ADP framework. If this is not successful either, then we try to use the direct application of polynomial interpretations from KG23.
The concrete implementation of the ADP framework for AST and the strategy for the use of the different processors is very similar to the original non-probabilistic DP framework and the ADP framework for innermost AST in KDG24. We first use the processors that do not rely on finding an interpretation (i.e., every processor except the reduction pair processor) until we cannot use them anymore to decrease the size of the problem. Then we use the reduction pair processor to delete some (or all) of the annotations from the annotated dependency pairs, and then we begin our strategy from the start and use the other processors again. Furthermore, changing to the non-probabilistic DP framework if there are only trivial probabilities is always preferred over the probabilistic reduction pair processor.
For the dependency graph and the usable terms, AProVE uses the same over-approximations as for the dependency graph in the non-probabilistic setting.
For the reduction pair processor, we currently only search for polynomials with coefficients in the range of at most {0,…,10}.
Finally, for PAST and innermost PAST (iPAST), we use the polynomial interpretation technique from ADY20 that is also implemented in the tool NaTT 2. However, in contrast to NaTT 2 we only consider natural polynomials and do not allow for rational or even real coefficients in the polynomials.
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 by executing
java -ea -jar aprove.jar -m wst pgcl.ari
or 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 pgcl.ari -p plain
java -ea -jar aprove.jar -m wst pgcl.ari -p html
One can also use the option -t limit to set the maximum time to search for a termination proof in seconds, e.g.,
java -ea -jar aprove.jar -m wst pgcl.ari -p html -t 30
To evaluate the power of our approach we used the existing set of 118 benchmarks from the website for the paper KFG24. However, this benchmark set contains almost no examples with overlapping rules and non-determinism. To demonstrate the strengths of our new ADP framework for AST compared to the method from KFG24, we added 12 new benchmarks including all examples from our paper.
For a more detailed explanation of every single benchmark see here. The full set of all 130 benchmarks can be downloaded here.
In the following table, we compare AProVE’s results for AST on arbitrary start terms when using our new ADP framework for AST directly, when using the method from KFG24 to switch to innermost AST and the corresponding ADP framework for innermost AST from KDG24, and when using the direct application of polynomials from KG23.
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 AST 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 AST 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 AST yet.
As in the Termination Competition, a timeout of 300 seconds was used for each example.
The following table shows the overall results for arbitrary start terms.
The numbers in brackets indicate the number of AST proofs for the 12 new examples.
| Examples | POLO | KFG24 | new AProVE |
|---|---|---|---|
| 130 | 37 (1) | 50 (1) | 58 (6) |
A detailed table with the result for each individual new benchmark can be downloaded here.
Finally, we also give a table to show the overall results for basic start terms:
| Examples | POLO | KFG24 | new AProVE |
|---|---|---|---|
| 130 | 37 (1) | 62 (1) | 74 (8) |