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.

翻译：依赖对是自动分析项重写系统终止性最强大的技术之一。我们将依赖对框架适配到概率场景中，以证明概率项重写系统的几乎必然最内终止性。为评估其能力，我们在工具AProVE中实现了该新框架。