There are many evaluation strategies for term rewrite systems, but proving termination automatically is usually easiest for innermost rewriting. Several syntactic criteria exist when innermost termination implies full termination. We adapt these criteria to the probabilistic setting, e.g., we show when it suffices to analyze almost-sure termination (AST) w.r.t. innermost rewriting to prove full AST of probabilistic term rewrite systems (PTRSs). These criteria also apply to other notions of termination like positive AST. We implemented and evaluated our new contributions in the tool AProVE.

翻译：项重写系统有多种评价策略，但自动证明终止性通常对内层重写最为简便。目前已存在若干句法准则，用于判定内层终止性何时可推导出全局终止性。我们将这些准则推广至概率设置，例如，我们证明了在何种条件下，只需分析内层重写的几乎必然终止性即可证明概率项重写系统的全局几乎必然终止性。这些准则同样适用于其他终止性概念，如正向几乎必然终止性。我们在工具AProVE中实现并评估了这些新贡献。