Document Open Access Logo

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

Authors Ugo Dal Lago , Guido Fiorillo , Paolo Pistone

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.34.pdf
  • Filesize: 0.91 MB
  • 27 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Verification by model checking
Keywords
  • Probabilistic λ-calculus
  • linear logic
  • weighted relational model
  • algebraic power series

Metrics

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.LICS.2026.34

Author Details

Ugo Dal Lago
  • University of Bologna, Italy
  • INRIA Sophia Antipolis, France
Guido Fiorillo
  • Université Claude Bernard Lyon 1, France
Paolo Pistone
  • Université Claude Bernard Lyon 1, France

Funding

  • Dal Lago, Ugo: funded by ANR-24-CE48-5521-01.
  • Fiorillo, Guido: funded by ANR-23-CPJ1-0054-01.
  • Pistone, Paolo: funded by ANR-23-CPJ1-0054-01.

References

  1. Jared Adams, Eric Freden, and Marni Mishna. From indexed grammars to generating functions. RAIRO Theor. Informatics Appl., 47(4):325-350, 2013. URL: https://doi.org/10.1051/ITA/2013041.
  2. Alfred V. Aho. Indexed grammars-an extension of context free grammars. In 8th Annual Symposium on Switching and Automata Theory, Austin, Texas, USA, October 18-20, 1967, pages 21-31. IEEE Computer Society, 1967. URL: https://doi.org/10.1109/FOCS.1967.16.
  3. Krzysztof R. Apt and Dexter C. Kozen. Limits for automatic verification of finite-state concurrent systems. Information Processing Letters, 22(6):307-309, 1986. URL: https://doi.org/10.1016/0020-0190(86)90071-2.
  4. Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui. A semantic account of metric preservation. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL '17, pages 545-556, New York, NY, USA, 2017. Association for Computing Machinery. URL: https://doi.org/10.1145/3009837.3009890.
  5. Christel Baier and Joost-Pieter Katoen. Principles of Model-Checking. The MIT Press, 2008. Google Scholar
  6. Cyril Banderier and Michael Drmota. Formulae and asymptotics for coefficients of algebraic functions. Combinatorics, Probability and Computing, 24(1):1-53, 2015. URL: https://doi.org/10.1017/S0963548314000728.
  7. Davide Barbarossa and Paolo Pistone. Tropical mathematics and the lambda-calculus II: Tropical geometry of probabilistic programming languages. Proc. ACM Program. Lang., 10(POPL), 2026. URL: https://doi.org/10.1145/3776675.
  8. Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. A core quantitative coeffect calculus. In Proceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 8410, pages 351-370, Berlin, Heidelberg, 2014. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-54833-8_19.
  9. Arnaud Carayol and Olivier Serre. Higher-order recursion schemes and their automata models. In Jean-Éric Pin, editor, Handbook of Automata Theory, pages 1295-1341. European Mathematical Society Publishing House, Zürich, Switzerland, 2021. URL: https://doi.org/10.4171/AUTOMATA-2/13.
  10. N. Chomsky and M.P. Schützenberger. The algebraic theory of context-free languages*. In P. Braffort and D. Hirschberg, editors, Computer Programming and Formal Systems, volume 35 of Studies in Logic and the Foundations of Mathematics, pages 118-161. Elsevier, 1963. URL: https://doi.org/10.1016/S0049-237X(08)72023-8.
  11. D.V Chudnovsky and G.V Chudnovsky. On expansion of algebraic functions in power and puiseux series, i. Journal of Complexity, 2(4):271-294, 1986. URL: https://doi.org/10.1016/0885-064X(86)90006-3.
  12. Pierre Clairambault, Charles Grellois, and Andrzej S. Murawski. Linearity in higher-order recursion schemes. Proc. ACM Program. Lang., 2(POPL):39:1-39:29, 2018. URL: https://doi.org/10.1145/3158127.
  13. Pierre Clairambault and Andrzej S. Murawski. On the expressivity of linear recursion schemes. In Peter Rossmanith, Pinar Heggernes, and Joost-Pieter Katoen, editors, 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019, Aachen, Germany, August 26-30, 2019, volume 138 of LIPIcs, pages 50:1-50:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.MFCS.2019.50.
  14. Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis. Model checking: algorithmic verification and debugging. Commun. ACM, 52(11):74-84, 2009. URL: https://doi.org/10.1145/1592761.1592781.
  15. Ugo Dal Lago, Guido Fiorillo, and Paolo Pistone. On higher-order probabilistic verification via the weighted relational model of linear logic, 2026. URL: https://arxiv.org/abs/2604.27986.
  16. Manfred Droste and Werner Kuich. Semirings and Formal Power Series, pages 3-28. Springer Berlin Heidelberg, Berlin, Heidelberg, 2009. URL: https://doi.org/10.1007/978-3-642-01492-5_1.
  17. Thomas Ehrhard. Differentials and distances in probabilistic coherence spaces. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, Dortmund, Germany, June 24-30, 2019, volume 131 of LIPIcs, pages 17:1-17:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.17.
  18. Thomas Ehrhard, Michele Pagani, and Christine Tasson. Full abstraction for probabilistic PCF. J. ACM, 65(4):23:1-23:44, 2018. URL: https://doi.org/10.1145/3164540.
  19. Javier Esparza, Antonin Kucera, and Richard Mayr. Model checking probabilistic pushdown automata. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, LICS '04, pages 12-21, USA, 2004. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2004.1319596.
  20. Kousha Etessami and Mihalis Yannakakis. Recursive markov chains, stochastic grammars, and monotone systems of nonlinear equations. J. ACM, 56(1):1:1-1:66, 2009. URL: https://doi.org/10.1145/1462153.1462154.
  21. Kousha Etessami and Mihalis Yannakakis. Model checking of recursive probabilistic systems. ACM Trans. Comput. Logic, 13(2), 2012. URL: https://doi.org/10.1145/2159531.2159534.
  22. Philippe Flajolet and Robert Sedgewick. Analytic Combinatorics. Cambridge University Press, 2009. URL: http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=9780521898065.
  23. Zeinab Galal and Jean-Simon Pacaud Lemay. Combining fixpoint and differentiation theory. In Pawel Sobocinski, Ugo Dal Lago, and Javier Esparza, editors, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, July 8-11, 2024, pages 37:1-37:14. ACM, 2024. URL: https://doi.org/10.1145/3661814.3662108.
  24. Dan R. Ghica and Alex I. Smith. Bounded linear types in a resource semiring. In Proceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 8410, pages 331-350, Berlin, Heidelberg, 2014. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-54833-8_18.
  25. Jean-Yves Girard. Normal functors, power series and λ-calculus. Annals of Pure and Applied Logic, 37(2):129-177, 1988. URL: https://doi.org/10.1016/0168-0072(88)90025-5.
  26. Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. Bounded linear logic: a modular approach to polynomial-time computability. Theoretical Computer Science, 97(1):1-66, 1992. URL: https://doi.org/10.1016/0304-3975(92)90386-T.
  27. Charles Grellois and Paul-André Melliès. Finitary semantics of linear logic and higher-order model-checking. In Giuseppe F. Italiano, Giovanni Pighizzini, and Donald Sannella, editors, Mathematical Foundations of Computer Science 2015 - 40th International Symposium, MFCS 2015, Milan, Italy, August 24-28, 2015, Proceedings, Part I, volume 9234 of Lecture Notes in Computer Science, pages 256-268. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-48057-1_20.
  28. Charles Grellois and Paul-André Melliès. Relational semantics of linear logic and higher-order model checking. In Stephan Kreutzer, editor, 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, Berlin, Germany, September 7-10, 2015, volume 41 of LIPIcs, pages 260-276. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.CSL.2015.260.
  29. Masahito Hasegawa. On traced monoidal closed categories. Math. Struct. Comput. Sci., 19(2):217-244, 2009. URL: https://doi.org/10.1017/S0960129508007184.
  30. Gerard J. Holzmann. The model checker spin. IEEE Trans. Softw. Eng., 23(5):279-295, 1997. URL: https://doi.org/10.1109/32.588521.
  31. André Joyal. Une théorie combinatoire des séries formelles. Advances in Mathematics, 42(1):1-82, 1981. URL: https://doi.org/10.1016/0001-8708(81)90052-9.
  32. Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. On the hardness of analyzing probabilistic programs. Acta Informatica, 56(3):255-285, 2019. URL: https://doi.org/10.1007/S00236-018-0321-1.
  33. Manuel Kauers and Peter Paule. The Concrete Tetrahedron - Symbolic Sums, Recurrence Equations, Generating Functions, Asymptotic Estimates. Texts & Monographs in Symbolic Computation. Springer, 2011. URL: https://doi.org/10.1007/978-3-7091-0445-3.
  34. Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, and Tobias Winkler. Generating functions for probabilistic programs. In Theoretical Computer Science and General Issues, volume 12561, pages 231-248. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-68446-4_12.
  35. Lutz Klinkenberg, Christian Blumenthal, Mingshuai Chen, Darion Haase, and Joost-Pieter Katoen. Exact bayesian inference for loopy probabilistic programs using generating functions. Proceedings of the ACM on programming languages, 8(OOPSLA1):pages 127, 2024. URL: https://doi.org/10.1145/3649844.
  36. Naoki Kobayashi, Ugo Dal Lago, and Charles Grellois. On the termination problem for probabilistic higher-order recursive programs. Log. Methods Comput. Sci., 16(4), 2020. URL: https://lmcs.episciences.org/6817.
  37. Werner Kuich and Arto Salomaa. Semirings, Automata, Languages, volume 5 of EATCS Monographs on Theoretical Computer Science. Springer, 1986. URL: https://doi.org/10.1007/978-3-642-69959-7.
  38. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. Prism: Probabilistic symbolic model checker. In Proceedings of the 12th International Conference on Computer Performance Evaluation, Modelling Techniques and Tools, TOOLS '02, pages 200-204, Berlin, Heidelberg, 2002. Springer-Verlag. URL: https://doi.org/10.1007/3-540-46029-2_13.
  39. Ugo Lago and Martin Hofmann. Bounded linear logic, revisited. In Proceedings of the 9th International Conference on Typed Lambda Calculi and Applications, TLCA '09, pages 80-94, Berlin, Heidelberg, 2009. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-02273-9_8.
  40. Jim Laird, Giulio Manzonetto, Guy McCusker, and Michele Pagani. Weighted relational models of typed lambda-calculi. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 301-310. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/LICS.2013.36.
  41. François Lamarche. Quantitative domains and infinitary algebras. Theoretical Computer Science, 94(1):37-62, 1992. URL: https://doi.org/10.1016/0304-3975(92)90323-8.
  42. Guanyan Li, Andrzej S. Murawski, and Luke Ong. Probabilistic verification beyond context-freeness. In Christel Baier and Dana Fisman, editors, LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, pages 33:1-33:13. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533351.
  43. David Marker. Model Theory : An Introduction. Graduate Texts in Mathematics. Springer, New York, NY, 2002 edition, August 2002. Google Scholar
  44. C.-H. L. Ong. On model-checking trees generated by higher-order recursion schemes. In Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, LICS '06, pages 81-90, USA, 2006. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2006.38.
  45. Luke Ong. Higher-order model checking: An overview. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 1-15. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.9.
  46. K. Vijay-Shanker, David J. Weir, and Aravind K. Joshi. Characterizing structural descriptions produced by various grammatical formalisms. In Candy L. Sidner, editor, 25th Annual Meeting of the Association for Computational Linguistics, Stanford University, Stanford, California, USA, July 6-9, 1987, pages 104-111. ACL, 1987. URL: https://doi.org/10.3115/981175.981190.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact