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