Recently, the well-known dependency pair (DP) framework was adapted to a dependency tuple framework in order to prove almost-sure innermost termination (iAST) of probabilistic term rewrite systems. While this approach was incomplete, in this paper, we improve it into a complete criterion for iAST by presenting a new, more elegant definition of DPs for probabilistic term rewriting. Based on this, we extend the probabilistic DP framework by new transformations. Our implementation in the tool AProVE shows that they increase its power considerably.

翻译：摘要：近期，为证明概率项重写系统的几乎必然最内终止性（iAST），研究者将经典的依赖对（DP）框架适配为依赖元组框架。尽管该方法是不可完备的，本文通过提出概率项重写中依赖对的全新、更简洁定义，将其改进为iAST的完备判定准则。基于此，我们通过新增变换扩展了概率DP框架。在AProVE工具中的实现表明，这些变换显著提升了其处理能力。