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的完全判定准则。在此基础上，我们通过新的变换扩展了概率依赖对框架。在工具AProVE中的实现表明，这些变换显著提升了其处理能力。