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

Ugo Dal Lago, Guido Fiorillo, Paolo Pistone

The problem of determining whether a probabilistic program terminates almost surely (i.e.~with probability one) is undecidable, and actually ${\Pi }_2^0$-complete. For this reason, a gr…