Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs

TL;DR

This paper extends the dependency pair technique to probabilistic term rewriting systems to automatically prove almost-sure innermost termination, implemented in the AProVE tool.

Contribution

It introduces a novel probabilistic dependency pair framework for termination analysis and provides an implementation in AProVE.

Findings

Successfully proved almost-sure innermost termination for probabilistic TRSs

Extended dependency pair framework to probabilistic settings

Implemented and tested in the AProVE tool

Abstract

Dependency pairs are one of the most powerful techniques to analyze termination of term rewrite systems (TRSs) automatically. We adapt the dependency pair framework to the probabilistic setting in order to prove almost-sure innermost termination of probabilistic TRSs. To evaluate its power, we implemented the new framework in our tool AProVE.