Dependency pairs (DPs) are one of the most powerful techniques for automated termination analysis of term rewrite systems. Recently, we adapted the DP framework to the probabilistic setting to prove almost-sure termination ( \(\texttt{AST}\) ) via annotated DPs (ADPs). However, this adaption only handled \(\texttt{AST}\) w.r.t. the innermost evaluation strategy. In this paper, we improve the ADP framework to prove \(\texttt{AST}\) for full rewriting. Moreover, we refine the framework for rewrite sequences that start with basic terms containing a single defined function symbol. We implemented and evaluated the new framework in our tool AProVE.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Annotated Dependency Pairs for Full Almost-Sure Termination of Probabilistic Term Rewriting

  • Jan-Christoph Kassing,
  • Jürgen Giesl

摘要

Dependency pairs (DPs) are one of the most powerful techniques for automated termination analysis of term rewrite systems. Recently, we adapted the DP framework to the probabilistic setting to prove almost-sure termination ( \(\texttt{AST}\) ) via annotated DPs (ADPs). However, this adaption only handled \(\texttt{AST}\) w.r.t. the innermost evaluation strategy. In this paper, we improve the ADP framework to prove \(\texttt{AST}\) for full rewriting. Moreover, we refine the framework for rewrite sequences that start with basic terms containing a single defined function symbol. We implemented and evaluated the new framework in our tool AProVE.