Using Stochastic Context-Free Grammars to Decide Almost-Sure Termination for Probabilistic Term Rewriting Systems
Abstract
Since term rewriting systems are Turing-complete, their termination is generally undecidable. The same holds for probabilistic term rewriting systems with respect to the property of almost sure termination (i.e., termination with probability one). This thesis investigates a specific class of probabilistic term rewriting systems which we named GNT that is syntactically restricted to be ground (i.e., all rewrite rules operate on terms without variables), non-overlapping (i.e., each term at each position matches at most one rewrite rule, eliminating ambiguity in rule selection) and tail-recursive (i.e., rewrite rules produce no nested recursive subterms). We show that for GNT, the problem of deciding almost sure termination can be reduced to checking consistency in stochastic context-free grammars. Stochastic context-free grammars, originally developed in formal language theory, generate strings via probabilistic derivations. Consistency in this context means that the probability of producing a string is one. Because consistency is efficiently decidable, this reduction yields a practical decision procedure for almost sure termination in the class GNT. Additionally we show that we can lessen the restriction of groundness to right-groundness (i.e., all rewrite rules produce terms without variables) in the context of innermost almost-sure termination (i.e., almost-sure termination using an innermost rewriting strategy, which rewrites nested reducible expression first). We implemented all of our results in the Automated Program Verification Environment (AProVE) and were able to return new negative results for some systems out of the Termination Competition (termCOMP) 2025 that AProVE could previously not analyze, i.e., we could prove that they were not almost-surely terminating.
Full text (PDF)· The results are also the basis of the VeriProP 2026 extended abstract.