Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Complete Dependency Pair Framework for Almost-Sure Innermost Termination of Probabilistic Term Rewriting

Jan-Christoph Kassing, Stefan Dollase, Jürgen Giesl

TL;DR

The paper tackles automatic verification of almost-sure innermost termination ($\mathrm{iAST}$) for probabilistic term rewriting systems by introducing a complete criterion based on annotated dependency pairs (ADP), replacing the previous dependency tuple (DT) approach. It defines a probabilistic ADP framework with a refined rewrite relation and chain-tree semantics, and develops a family of sound and complete processors to transform ADP problems into simpler subproblems. The authors adapt the DP framework to the probabilistic setting, including new processors and transformational techniques, and prove the completeness of the resulting ADP-based chain criterion. Their implementation in AProVE demonstrates substantial power gains over prior methods, enabling proofs for challenging PTRSs (e.g., probabilistic quicksort) and expanding automatic iAST coverage on standard benchmark suites.

Abstract

Recently, the well-known dependency pair (DP) framework was adapted to a dependency tuple framework in order to prove almost-sure innermost termination (iAST) of probabilistic term rewrite systems. While this approach was incomplete, in this paper, we improve it into a complete criterion for iAST by presenting a new, more elegant definition of DPs for probabilistic term rewriting. Based on this, we extend the probabilistic DP framework by new transformations. Our implementation in the tool AProVE shows that they increase its power considerably.

A Complete Dependency Pair Framework for Almost-Sure Innermost Termination of Probabilistic Term Rewriting

TL;DR

The paper tackles automatic verification of almost-sure innermost termination () for probabilistic term rewriting systems by introducing a complete criterion based on annotated dependency pairs (ADP), replacing the previous dependency tuple (DT) approach. It defines a probabilistic ADP framework with a refined rewrite relation and chain-tree semantics, and develops a family of sound and complete processors to transform ADP problems into simpler subproblems. The authors adapt the DP framework to the probabilistic setting, including new processors and transformational techniques, and prove the completeness of the resulting ADP-based chain criterion. Their implementation in AProVE demonstrates substantial power gains over prior methods, enabling proofs for challenging PTRSs (e.g., probabilistic quicksort) and expanding automatic iAST coverage on standard benchmark suites.

Abstract

Recently, the well-known dependency pair (DP) framework was adapted to a dependency tuple framework in order to prove almost-sure innermost termination (iAST) of probabilistic term rewrite systems. While this approach was incomplete, in this paper, we improve it into a complete criterion for iAST by presenting a new, more elegant definition of DPs for probabilistic term rewriting. Based on this, we extend the probabilistic DP framework by new transformations. Our implementation in the tool AProVE shows that they increase its power considerably.
Paper Structure (2 sections, 1 theorem, 2 equations)

This paper contains 2 sections, 1 theorem, 2 equations.

Table of Contents

  1. Introduction
  2. The DP Framework

Key Result

theorem thmcountertheorem

For the SCCs $\mathcal{P}_1, \ldots, \mathcal{P}_n$ of the $(\mathcal{P}, \mathcal{R})$-dependency graph, $\operatorname{Proc}_{\mathtt{DG}}(\mathcal{P},\mathcal{R}) = \{(\mathcal{P}_1,\mathcal{R}), \ldots, (\mathcal{P}_n,\mathcal{R})\}$ is sound and complete.

Theorems & Definitions (1)

  • theorem thmcountertheorem: Dependency Graph Processor