Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs

2023/05/19 by Jan-Christoph Kassing, Kassing, Jan-Christoph, Jürgen Giesl +1 · 2 citations
Computer Science · #Natural Language Processing Techniques #Semantic Web and Ontologies #Advanced Database Systems and Queries

paper · pdf · doi:10.48550/arxiv.2305.11741

Abstract

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.

Cited by

• The annotated dependency pair framework for almost-sure termination of probabilistic term rewriting
• Dependency Pairs for Expected Innermost Runtime Complexity and Strong Almost-Sure Termination of Probabilistic Term Rewriting

Related

• Dependency Tuples for Almost-Sure Innermost Termination of Probabilistic Term Rewriting (Short WST Version)
• A Complete Dependency Pair Framework for Almost-Sure Innermost Termination of Probabilistic Term Rewriting
• The Annotated Dependency Pair Framework for Almost-Sure Termination of Probabilistic Term Rewriting
• Dependency Pairs for Expected Innermost Runtime Complexity and Strong Almost-Sure Termination of Probabilistic Term Rewriting
• A Dependency Pair Framework for Relative Termination of Term Rewriting