The Annotated Dependency Pair Framework for Almost-Sure Termination of Probabilistic Term Rewriting
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909639593951232 |
|---|---|
| author | Kassing, Jan-Christoph Giesl, Jürgen |
| author_facet | Kassing, Jan-Christoph Giesl, Jürgen |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2412_20220 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | The Annotated Dependency Pair Framework for Almost-Sure Termination of Probabilistic Term Rewriting Kassing, Jan-Christoph Giesl, Jürgen Logic in Computer Science 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. |
| title | The Annotated Dependency Pair Framework for Almost-Sure Termination of Probabilistic Term Rewriting |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2412.20220 |