On Higher-Order Probabilistic Verification via the Weighted Relational Model of Linear Logic
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911636749549568 |
|---|---|
| author | Lago, Ugo Dal Fiorillo, Guido Pistone, Paolo |
| author_facet | Lago, Ugo Dal Fiorillo, Guido Pistone, Paolo |
| contents | The problem of determining whether a probabilistic program terminates almost surely (i.e.~with probability one) is undecidable, and actually $Π^0_2$-complete. For this reason, a growing literature has explored classes of programs for which this and related problems can be shown (semi-)decidable. In this work we consider the termination problem for the language of Probabilistic Higher-Order Recursion Schemes (PHORS). Using the weighted relational semantics of linear logic, we translate this problem into the computation of suitable generating functions associated with the program interpreted. This way, we establish the decidability of almost sure termination for a class of programs that extends Li et al.'s affine PHORS via a type discipline with bounded exponentials. To achieve this, we show that the generating functions for such programs are always algebraic, that is, solutions of polynomial equations, yielding an effective method to answer the termination problem. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_27986 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | On Higher-Order Probabilistic Verification via the Weighted Relational Model of Linear Logic Lago, Ugo Dal Fiorillo, Guido Pistone, Paolo Logic in Computer Science F.3.2; F.4.1 The problem of determining whether a probabilistic program terminates almost surely (i.e.~with probability one) is undecidable, and actually $Π^0_2$-complete. For this reason, a growing literature has explored classes of programs for which this and related problems can be shown (semi-)decidable. In this work we consider the termination problem for the language of Probabilistic Higher-Order Recursion Schemes (PHORS). Using the weighted relational semantics of linear logic, we translate this problem into the computation of suitable generating functions associated with the program interpreted. This way, we establish the decidability of almost sure termination for a class of programs that extends Li et al.'s affine PHORS via a type discipline with bounded exponentials. To achieve this, we show that the generating functions for such programs are always algebraic, that is, solutions of polynomial equations, yielding an effective method to answer the termination problem. |
| title | On Higher-Order Probabilistic Verification via the Weighted Relational Model of Linear Logic |
| topic | Logic in Computer Science F.3.2; F.4.1 |
| url | https://arxiv.org/abs/2604.27986 |