Dependency Tuples for Almost-Sure Innermost Termination of Probabilistic Term Rewriting (Short WST Version)

TL;DR

This paper extends the dependency pair framework to probabilistic term rewrite systems to automatically prove almost-sure innermost termination, with implementation in the AProVE tool.

Contribution

It introduces a novel adaptation of dependency pairs for probabilistic TRSs and demonstrates its effectiveness through implementation.

Findings

Successfully adapted dependency pairs to probabilistic TRSs

Implemented the framework in AProVE for automatic analysis

Proved almost-sure innermost termination in probabilistic settings

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.