The Annotated Dependency Pair Framework for Almost-Sure Termination of Probabilistic Term Rewriting

TL;DR

This paper introduces an annotated dependency pair framework adapted for probabilistic term rewrite systems, enabling automatic proof of almost-sure termination, and implements it in the AProVE tool.

Contribution

It extends dependency pair techniques to probabilistic rewriting and provides an automated method for almost-sure termination analysis.

Findings

Framework successfully proves almost-sure termination

Implementation in AProVE demonstrates practical applicability

Applicable to both full and innermost rewriting strategies

Abstract

Dependency pairs are one of the most powerful techniques to analyze termination of term rewrite systems automatically. We adapt dependency pairs to the probabilistic setting and develop an annotated dependency pair framework for automatically proving almost-sure termination of probabilistic term rewrite systems, both for full and innermost rewriting. To evaluate its power, we implemented our framework in the tool AProVE.