From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting

TL;DR

This paper adapts syntactic criteria from deterministic to probabilistic term rewriting to automatically prove almost-sure termination, enhancing the analysis of probabilistic systems with practical implementation in AProVE.

Contribution

It introduces criteria for inferring full almost-sure termination of probabilistic term rewrite systems from innermost termination analysis.

Findings

Criteria successfully applied to PTRSs

Implementation in AProVE demonstrates effectiveness

Extends termination analysis to probabilistic rewriting

Abstract

There are many evaluation strategies for term rewrite systems, but proving termination automatically is usually easiest for innermost rewriting. Several syntactic criteria exist when innermost termination implies full termination. We adapt these criteria to the probabilistic setting, e.g., we show when it suffices to analyze almost-sure termination (AST) w.r.t. innermost rewriting to prove full AST of probabilistic term rewrite systems (PTRSs). These criteria also apply to other notions of termination like positive AST. We implemented and evaluated our new contributions in the tool AProVE.