Recently, we adapted the well-known dependency pair (DP) framework to a dependency tuple (DT) framework in order to prove almost-sure innermost termination (iAST) of probabilistic term rewriting systems. In this paper, we improve this approach into a complete criterion for iAST by considering positions of subterms. Based on this, we extend the probabilistic DT framework by new transformations. Our implementation in the tool AProVE shows that they increase its power substantially.

翻译：近期，我们将经典的依赖对（DP）框架适配为依赖元组（DT）框架，以证明概率项重写系统的几乎必然最内终止（iAST）。本文通过考虑子项位置，将这一方法改进为iAST的完备判据。基于此，我们通过新变换扩展了概率DT框架。在工具AProVE中的实现表明，这些扩展显著提升了其性能。