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.

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