DROPS

Document

DOI: 10.4230/LIPIcs.LICS.2026.34

On Higher-Order Probabilistic Verification via the Weighted Relational Model of Linear Logic

Authors: Ugo Dal Lago, Guido Fiorillo, and Paolo Pistone

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract

The problem of determining whether a probabilistic program terminates almost surely (i.e. with probability one) is undecidable, and actually Π⁰₂-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.

Cite as

Ugo Dal Lago, Guido Fiorillo, and Paolo Pistone. On Higher-Order Probabilistic Verification via the Weighted Relational Model of Linear Logic. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 34:1-34:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{dallago_et_al:LIPIcs.LICS.2026.34,
  author =	{Dal Lago, Ugo and Fiorillo, Guido and Pistone, Paolo},
  title =	{{On Higher-Order Probabilistic Verification via the Weighted Relational Model of Linear Logic}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{34:1--34:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.34},
  URN =		{urn:nbn:de:0030-drops-268211},
  doi =		{10.4230/LIPIcs.LICS.2026.34},
  annote =	{Keywords: Probabilistic \lambda-calculus, linear logic, weighted relational model, algebraic power series}
}

Search Results

Documents authored by Fiorillo, Guido

On Higher-Order Probabilistic Verification via the Weighted Relational Model of Linear Logic

Abstract

Cite as

Thanks for your feedback!

Could not send message