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.

翻译：近年来，已发展出多种自动证明各类概率程序终止性的技术。然而，目前鲜有自动方法能够反驳其终止性。本文提出了首套自动反驳概率项重写系统（正）几乎必然终止性的技术。反驳非概率系统的终止性需要找到无限计算的有限表示，例如重写系统的循环。我们将此类定性技术拓展至概率项重写领域，该领域需要进行定量分析。除了循环的存在性外，我们还需统计此类循环的数量，以便在计算中嵌入合适的随机游走，从而反驳终止性。为评估其效能，我们在工具AProVE中实现了所有技术。