A First Decision Procedure for Almost-Sure Termination of Probabilistic Term Rewriting
Authors: J.-C. Kassing, A. Scheid, H. Nagel, and J. Giesl
While termination of ordinary programs has been studied for decades, the analysis of probabilistic programs has become increasingly important. In the probabilistic setting, requiring all executions to be finite is often too restrictive. Instead, one studies almost-sure termination (AST) where every computation has to terminate with probability 1. Thus, infinite executions may still exist, but the probability of such an infinite execution is 0. We present the first decision procedure for almost-sure termination of a non-trivial subclass of probabilistic term rewrite systems (PTRSs): we show how to automatically transform every PTRS that is right-ground, non-overlapping, and tail-recursive into a stochastic context-free grammar with the same termination behavior, for which almost-sure termination is decidable.