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

RWTH Publications (RWTH Aachen)

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.

Authors 2

1. Jan-Christoph Kassing Aachen LuFG Informatik 2

   RWTH Aachen University

   Affiliation as printed

   LuFG Informatik 2 , RWTH Aachen University , Germany

2. Jürgen Giesl Aachen LuFG Informatik 2

   RWTH Aachen University

   Affiliation as printed

   LuFG Informatik 2 , RWTH Aachen University , Germany