AProVE Update: New Version Available
We are pleased to announce a new release of AProVE, featuring novel techniques for the analysis of probabilistic term rewrite systems.
What’s New?
The latest version of AProVE now supports automated techniques for disproving probabilistic termination, including almost-sure termination (AST) and positive almost-sure termination (PAST), for probabilistic term rewrite systems (PTRSs). A PTRS is AST if the probability of termination is 1, and a PTRS is PAST if the expected length of every evaluation is finite.
Disproving termination of non-probabilistic rewrite systems requires finding a finite representation of an infinite computation, e.g., a loop of the rewrite system. We extend such qualitative techniques to probabilistic term rewriting, where a quantitative analysis is required. In addition to the existence of a loop, we have to count the number of such loops in order to embed suitable random walks into a computation, thereby disproving AST or PAST. Embedding random walks into the computation of a PTRS gives insights on the behavior of the PTRS via a well-studied stochastic process, where termination is easy to analyze.
What is a Random Walk?
Random walks (also known as drunkard’s walks) are a special form of stochastic processes. Think about Frank, a drunk person that tries to go home after a public folk festival. For simplicity, we assume that his way home is a simple line. Since Frank is drunk, there is only a 50% chance that he moves towards his home. In the other 50% he takes a step backwards, away from home. This behavior is described by the symmetric random walk μ depicted above on the right. Here, Frank starts at position 1 and his home is at position 0. Even though there is the possibility that Frank will never reach his home (he can move away from 0 in every single step), the probability of this to happen is 0. Therefore, Frank will reach his home with probability 1. However, he has to take an infinite number of steps in expectation.
What is Depicted in the Figure Above?
The figure at the top illustrates how a symmetric random walk μ can be embedded into the rewrite sequence tree of a PTRS P by counting the number of g-symbols within terms. On the left, one can see a possible computation of a P that rewrites a term with a single g-symbol into either a term without any g-symbols (with a chance of 1/2) or into a term containing two g-symbols (with a chance of 1/2). The dashed lines show how this corresponds to the computation of the symmetric random walk μ, which is known to be not PAST. Therefore, this embedding disproves PAST for P. If you are interested in details on how this embedding works precisely and how to find it automatically, check out our new research paper.
How to Try It
The easiest way to run AProVE is through the web interface: for PTRSs in WST format and for PTRSs in ARI format.
The newest version is available for download on GitHub as well.
AProVE analyzes SAST instead of PAST!
Our implementation in the tool AProVE only allows the user to analyze AST or SAST, but one cannot select PAST. A PTRS is strongly or bounded almost-surely terminating (SAST) if for every term t there is a finite bound on the expected lengths of all evaluations starting in t. Thus, if there is a start term t which non-deterministically leads to evaluations of arbitrary finite length, then the program can be PAST, but not SAST. In general, SAST implies PAST, and PAST implies AST, but the converse directions do not hold.
At first sight, one might think that all three notions are interesting and worth investigating. However, it was shown in [KG25] that PAST and SAST coincide for almost all PTRSs. For example, if the signature contains at least one function symbol of arity greater than 1, then there is no difference between PAST and SAST for finite PTRSs. Since AProVE only analyzes finite rewrite systems, we decided to omit an implementation that focuses specifically on PAST.
Next Milestone: Open Source
Although our schedule experienced a slight delay, we are excited to announce that the open-source release of AProVE is on the way. This update marks the final release before AProVE becomes open source. Expect it to happen at the beginning of March.
To get notified when AProVE becomes open-source, become a member of our mailing list. For this, please send an email with “subscribe” in the subject line to aprove-news-join@lists.rwth-aachen.de .
— The AProVE Team