Searcharxiv⌕ Search

arXiv subjects

Jan-Christoph Kassing

Publications and source records attributed to Jan-Christoph Kassing.

11 recordsLinked to original sources
arXiv2026

Disproving (Positive) Almost-Sure Termination of Probabilistic Term Rewriting via Random Walks

In recent years, numerous techniques were developed to automatically prove termination of different kinds of probabilistic programs. However, there are only few automated methods to disprove their termination. In this paper, we present the first techniques to automatically disprove (positive) almost-sure termination of probabilistic term rewrite systems. Disproving termination of non-probabilistic systems requires finding a finite representation of an infinite computation, e.g., a loop of the rewrite system. We extend such qualitative techniques to probabilistic term rewriting, where a quantitative analysis is required. In addition to the existence of a loop, we have to count the number of such loops in order to embed suitable random walks into a computation, thereby disproving termination. To evaluate their power, we implemented all our techniques in the tool AProVE.

cs.LO↗
arXiv2025

From Innermost to Full Probabilistic Term Rewriting: Almost-Sure Termination, Complexity, and Modularity

There are many evaluation strategies for term rewrite systems, but automatically proving termination or analyzing complexity is usually easiest for innermost rewriting. Several syntactic criteria exist when innermost termination implies (full) termination or when runtime complexity and innermost runtime complexity coincide. We adapt these criteria to the probabilistic setting, e.g., we show when it suffices to analyze almost-sure termination w.r.t. innermost rewriting in order to prove (full) almost-sure termination of probabilistic term rewrite systems. These criteria can be applied for both termination and complexity analysis in the probabilistic setting. We implemented and evaluated our new contributions in the tool AProVE. Moreover, we also use our new results to investigate the modularity of probabilistic termination properties.

cs.LO↗
arXiv2025

Dependency Pairs for Expected Innermost Runtime Complexity and Strong Almost-Sure Termination of Probabilistic Term Rewriting

The dependency pair (DP) framework is one of the most powerful techniques for automatic termination and complexity analysis of term rewrite systems. While DPs were extended to prove almost-sure termination of probabilistic term rewrite systems (PTRSs), automatic complexity analysis for PTRSs is largely unexplored. We introduce the first DP framework for analyzing expected complexity and for proving positive or strong almost-sure termination (SAST) of innermost rewriting with PTRSs, i.e., finite expected runtime. We implemented our framework in the tool AProVE and demonstrate its power compared to existing techniques for proving SAST.

cs.LO↗
arXiv2025

The Annotated Dependency Pair Framework for Almost-Sure Termination of Probabilistic Term Rewriting

Dependency pairs are one of the most powerful techniques to analyze termination of term rewrite systems automatically. We adapt dependency pairs to the probabilistic setting and develop an annotated dependency pair framework for automatically proving almost-sure termination of probabilistic term rewrite systems, both for full and innermost rewriting. To evaluate its power, we implemented our framework in the tool AProVE.

cs.LO↗
arXiv2025

Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems

We present novel semiring semantics for abstract reduction systems (ARSs). More precisely, we provide a weighted version of ARSs, where the reduction steps induce weights from a semiring. Inspired by provenance analysis in database theory and logic, we obtain a formalism that can be used for provenance analysis of arbitrary ARSs. Our semantics handle (possibly unbounded) non-determinism and possibly infinite reductions. Moreover, we develop several techniques to prove upper and lower bounds on the weights resulting from our semantics, and show that in this way one obtains a uniform approach to analyze several different properties like termination, derivational complexity, space complexity, safety, as well as combinations of these properties.

cs.LO↗
arXiv2025

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

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 (AST) via annotated DPs (ADPs). However, this adaption only handled AST w.r.t. the innermost evaluation strategy. In this paper, we improve the ADP framework to prove 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.

cs.LO↗
arXiv2024

A Dependency Pair Framework for Relative Termination of Term Rewriting

Dependency pairs are one of the most powerful techniques for proving termination of term rewrite systems (TRSs), and they are used in almost all tools for termination analysis of TRSs. Problem #106 of the RTA List of Open Problems asks for an adaption of dependency pairs for relative termination. Here, infinite rewrite sequences are allowed, but one wants to prove that a certain subset of the rewrite rules cannot be used infinitely often. Dependency pairs were recently adapted to annotated dependency pairs (ADPs) to prove almost-sure termination of probabilistic TRSs. In this paper, we develop a novel adaption of ADPs for relative termination. We implemented our new ADP framework in our tool AProVE and evaluate it in comparison to state-of-the-art tools for relative termination of TRSs.

cs.LO↗
arXiv2024

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

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.

cs.LO↗
arXiv2024

From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting

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.

cs.LO↗