Disproving (Positive) Almost-Sure Termination of Probabilistic Term Rewriting via Random Walks
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866916057183158272 |
|---|---|
| author | Kassing, Jan-Christoph Nagel, Henri Schlecht, Alexander Giesl, Jürgen |
| author_facet | Kassing, Jan-Christoph Nagel, Henri Schlecht, Alexander Giesl, Jürgen |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_16522 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Disproving (Positive) Almost-Sure Termination of Probabilistic Term Rewriting via Random Walks Kassing, Jan-Christoph Nagel, Henri Schlecht, Alexander Giesl, Jürgen Logic in Computer Science 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. |
| title | Disproving (Positive) Almost-Sure Termination of Probabilistic Term Rewriting via Random Walks |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2602.16522 |