Dependency Pairs for Expected Runtime Complexity of Probabilistic Term Rewriting
Authors: J.-C. Kassing, L. Spitzer, and J. Giesl
A probabilistic term rewrite system (PTRS) is strongly almost-surely terminating (SAST) if, for every term, the supremum over the expected number of rewrite steps of all possible reductions is finite. Currently, the only approach to analyze SAST of PTRSs automatically is the direct application of polynomial or matrix interpretations to the whole PTRS, which is limited in power. We develop the first dependency pair (DP) framework for SAST and expected innermost runtime complexity of PTRSs by lifting the DP framework for almost-sure termination accordingly, and implement it in the tool AProVE. This is an extended abstract of our PPDP ‘25 paper.