通过随机游走否定概率项重写系统的（正）几乎必然终止性
计算机科学中的逻辑
2026-05-29 v2
摘要
近年来发展了诸多技术来自动证明不同类型的概率程序的终止性。然而，几乎没有自动方法来否定它们的终止性。在本文中，我们提出了首批自动否定概率项重写系统（正）几乎必然终止性的技术。否定非概率系统的终止性需要找到一个表示无限计算的有限对象，例如重写系统的一个循环。我们将此类定性技术扩展到概率项重写，其中需要进行量化分析。除了循环的存在外，我们还需要计算此类循环的数量，以便在计算中嵌入合适的随机游走，从而否定终止性。为了评估其威力，我们将所有技术实现于工具AProVE中。
引用
@article{arxiv.2602.16522,
title = {Disproving (Positive) Almost-Sure Termination of Probabilistic Term Rewriting via Random Walks},
author = {Jan-Christoph Kassing and Henri Nagel and Alexander Schlecht and Jürgen Giesl},
journal= {arXiv preprint arXiv:2602.16522},
year = {2026}
}