×

On the termination problem for probabilistic higher-order recursive programs. (English) Zbl 1490.68134

Summary: In the last two decades, there has been much progress on model checking of both probabilistic systems and higher-order programs. In spite of the emergence of higher-order probabilistic programming languages, not much has been done to combine those two approaches. In this paper, we initiate a study on the probabilistic higher-order model checking problem, by giving some first theoretical and experimental results. As a first step towards our goal, we introduce PHORS, a probabilistic extension of higher-order recursion schemes (HORS), as a model of probabilistic higher-order programs. The model of PHORS may alternatively be viewed as a higher-order extension of recursive Markov chains. We then investigate the probabilistic termination problem – or, equivalently, the probabilistic reachability problem. We prove that almost sure termination of order-2 PHORS is undecidable. We also provide a fixpoint characterization of the termination probability of PHORS, and develop a sound (but possibly incomplete) procedure for approximately computing the termination probability. We have implemented the procedure for order-2 PHORSs, and confirmed that the procedure works well through preliminary experiments.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q45 Formal languages and automata

Software:

MoCHi
PDFBibTeX XMLCite
Full Text: arXiv Link

References:

[1] Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. In John P. Gallagher and Martin Sulzmann, editors,FLOPS 2018, volume 10818 ofLNCS, pages 132-148. Springer, 2018. · Zbl 1507.68140
[2] Tom´as Br´azdil, V´aclav Brozek, Vojtech Forejt, and Anton´ın Kucera. Branching-time modelchecking of probabilistic pushdown automata.J. Comput. Syst. Sci., 80(1):139-156, 2014. · Zbl 1311.68084
[3] Tom´as Br´azdil, Javier Esparza, Stefan Kiefer, and Anton´ın Kucera. Analyzing probabilistic pushdown automata.Formal Methods in System Design, 43(2):124-163, 2013. · Zbl 1291.68226
[4] Olivier Bournez and Florent Garnier. Proving positive almost-sure termination. In J¨urgen Giesl, editor,RTA 2005, volume 3467 ofLNCS, pages 323-337. Springer, 2005. · Zbl 1078.68057
[5] Christel Baier and Joost-Pieter Katoen.Principles of Model Checking. The MIT Press, 2008. · Zbl 1179.68076
[6] Christopher H. Broadbent and Naoki Kobayashi. Saturation-based model checking of higher-order recursion schemes. InCSL 2013, volume 23 ofLIPIcs, pages 129-148, 2013. · Zbl 1356.68141
[7] Flavien Breuvart and Ugo Dal Lago. On intersection types and probabilistic lambda calculi. In David Sabel and Peter Thiemann, editors,PPDP 2018, pages 8:1-8:13. ACM, 2018.
[8] Cristian Calude.Information and Randomness: An Algorithmic Perspective. Springer-Verlag, Berlin, Heidelberg, 2nd edition, 2002. · Zbl 1055.68058
[9] Rapha¨elle Crubill´e and Ugo Dal Lago. On probabilistic applicative bisimulation and call-by-value λ-calculi. In Zhong Shao, editor,ESOP 2014, volume 8410 ofLNCS, pages 209-228. Springer, 2014. · Zbl 1405.68076
[10] Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors.Handbook of Model Checking. Springer, 2018. · Zbl 1390.68001
[11] Krishnendu Chatterjee, Petr Novotn´y, and Dorde Zikelic. Stochastic invariants for probabilistic termination. In Giuseppe Castagna and Andrew D. Gordon, editors,POPL 2017, pages 145-160. ACM, 2017. · Zbl 1380.68114
[12] Patrick Cousot. Types as abstract interpretations. In Peter Lee, Fritz Henglein, and Neil D. Jones, editors,POPL 1997, pages 316-331. ACM Press, 1997.
[13] Aleksandar Chakarov and Sriram Sankaranarayanan. Probabilistic program analysis with martingales. In Natasha Sharygina and Helmut Veith, editors,CAV 2013, pages 511-526, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg.
[14] Vincent Danos and Russell Harmer. Probabilistic game semantics.ACM Trans. Comput. Log., 3(3):359-382, 2002. · Zbl 1365.68310
[15] Ugo Dal Lago and Charles Grellois. Probabilistic termination by monadic affine sized typing. In ESOP 2017, pages 393-419, 2017. · Zbl 1485.68045
[16] Karel de Leeuw, Edward F. Moore, Claude E. Shannon, and Norman Shapiro. Computability by probabilistic machines.Automata Studies, 34:183-212, 1956.
[17] Ugo Dal Lago, Davide Sangiorgi, and Michele Alberti. On coinductive equivalences for higherorder probabilistic functional programs. InPOPL 2014, pages 297-308, 2014. · Zbl 1284.68424
[18] Ugo Dal Lago and Margherita Zorzi. Probabilistic operational semantics for the lambda calculus. RAIRO - Theor. Inf. and Applic., 46(3):413-450, 2012. · Zbl 1279.68183
[19] Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Computing least fixed points of probabilistic systems of polynomials. InSTACS 2010, volume 5 ofLIPIcs, pages 359-370. Schloss Dagstuhl Leibniz-Zentrum f¨ur Informatik, 2010. · Zbl 1230.65022
[20] Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Proving termination of probabilistic programs using patterns. In P. Madhusudan and Sanjit A. Seshia, editors,CAV 2012, pages 123-138, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg.
[21] Thomas Ehrhard, Christine Tasson, and Michele Pagani. Probabilistic coherence spaces are fully abstract for probabilistic PCF. InPOPL 2014, pages 309-320, 2014. · Zbl 1284.68268
[22] 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. · Zbl 1325.68091
[23] Kousha Etessami and Mihalis Yannakakis. Model checking of recursive probabilistic systems. ACM Trans. Comput. Log., 13(2):12:1-12:40, 2012. · Zbl 1351.68159
[24] Kousha Etessami and Mihalis Yannakakis. Recursive Markov decision processes and recursive stochastic games.J. ACM, 62(2):11:1-11:69, 2015. · Zbl 1333.91005
[25] Luis Mar´ıa Ferrer Fioriti and Holger Hermanns. Probabilistic termination: Soundness, completeness, and compositionality. In Sriram K. Rajamani and David Walker, editors,POPL 2015, pages 489-501. ACM, 2015. · Zbl 1345.68104
[26] Shafi Goldwasser and Silvio Micali. Probabilistic encryption.J. Comput. Syst. Sci., 28(2):270-299, 1984. · Zbl 0563.94013
[27] Charles Grellois and Paul-Andr´e Melli‘es. Finitary semantics of linear logic and higher-order model-checking. In Italiano et al. [IPS15], pages 256-268. · Zbl 1465.68179
[28] Charles Grellois and Paul-Andr´e Melli‘es. Relational semantics of linear logic and higher-order model checking. InCSL 2015, volume 41 ofLIPIcs, pages 260-276. Schloss Dagstuhl - LeibnizZentrum fuer Informatik, 2015. · Zbl 1373.68287
[29] Hugo Gimbert and Youssouf Oualhadj. Probabilistic automata on finite words: Decidable and undecidable problems. In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide, and Paul G. Spirakis, editors,ICALP 2010, volume 6199 ofLNCS, pages 527-538. Springer, 2010. · Zbl 1288.68156
[30] Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. A convenient category for higher-order probability theory. InLICS 2017, pages 1-12. IEEE Computer Society, 2017. · Zbl 1395.68082
[31] Matthew Hague, Andrzej Murawski, C.-H. Luke Ong, and Olivier Serre. Collapsible pushdown automata and recursion schemes. InLICS 2008, pages 452-461. IEEE Computer Society, 2008. · Zbl 1407.68256
[32] John Hughes, Lars Pareto, and Amr Sabry. Proving the correctness of reactive systems using sized types. In Hans-Juergen Boehm and Guy L. Steele Jr., editors,POPL 1996, pages 410-423. ACM Press, 1996.
[33] Juraj Hromkovic.Design and Analysis of Randomized Algorithms - Introduction to Design Paradigms. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2005. · Zbl 1083.68146
[34] Giuseppe F. Italiano, Giovanni Pighizzini, and Donald Sannella, editors.MFCS 2015, volume 9234 ofLNCS. Springer, 2015.
[35] C. Jones and Gordon D. Plotkin. A probabilistic powerdomain of evaluations. InLICS 1989, pages 186-195. IEEE Computer Society, 1989. · Zbl 0716.06003
[36] Achim Jung and Regina Tix. The troublesome probabilistic powerdomain.ENTCS, 13:70 - 91, 1998. Comprox III, Third Workshop on Computation and Approximation. · Zbl 0917.68135
[37] Naoki Kobayashi, Ugo Dal Lago, and Charles Grellois. On the termination problem for probabilistic higher-order recursive programs. InProceedings of LICS 2019. IEEE, 2019. · Zbl 1490.68134
[38] Benjamin Lucien Kaminski and Joost-Pieter Katoen. On the hardness of almost-sure termination. In Italiano et al. [IPS15], pages 307-318. · Zbl 1465.68097
[39] Stefan Kiefer, Michael Luttenberger, and Javier Esparza. On the convergence of newton’s method for monotone systems of polynomial equations. InSTOC 2007, pages 217-226. ACM, 2007. · Zbl 1232.65076
[40] Teodor Knapik, Damian Niwinski, and Pawel Urzyczyn. Deciding monadic theories of hyperalgebraic trees. InTLCA 2001, volume 2044 ofLNCS, pages 253-267. Springer, 2001. · Zbl 0981.03012
[41] Teodor Knapik, Damian Niwinski, and Pawel Urzyczyn. Higher-order pushdown trees are easy. InFoSSaCS 2002, volume 2303 ofLNCS, pages 205-222. Springer, 2002. · Zbl 1077.03508
[42] Naoki Kobayashi and C.-H. Luke Ong. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. InLICS 2009, pages 179-188. IEEE Computer Society Press, 2009.
[43] Naoki Kobayashi and C.-H. Luke Ong. Complexity of model checking recursion schemes for fragments of the modal mu-calculus.LMCS, 7(4), 2011. · Zbl 1237.68124
[44] Naoki Kobayashi. Model-checking higher-order functions. InPPDP 2009, pages 25-36. ACM Press, 2009.
[45] Naoki Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. InPOPL 2009, pages 416-428. ACM Press, 2009. · Zbl 1315.68099
[46] Naoki Kobayashi. Model checking higher-order programs.J. ACM, 60(3), 2013. · Zbl 1281.68157
[47] Naoki Kobayashi. Inclusion between the frontier language of a non-deterministic recursive program scheme and the dyck language is undecidable.Theor. Comput. Sci., 777:409-416, 2019. · Zbl 1429.68120
[48] Gregory M. Kobele and Sylvain Salvati. The IO and OI hierarchies revisited.Inf. Comput., 243:205-221, 2015. · Zbl 1327.68145
[49] Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno. Predicate abstraction and CEGAR for higher-order model checking. InPLDI 2011, pages 222-233. ACM Press, 2011. · Zbl 1381.68035
[50] Yuri V. Matiyasevich.Hilbert’s Tenth Problem. The MIT Press, 1993. · Zbl 0790.03008
[51] Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen. A new proof rule for almost-sure termination.POPL 2018, pages 33:1-33:28, 2018.
[52] Andrzej S. Murawski and Jo¨el Ouaknine. On probabilistic program equivalence and refinement. InCONCUR 2005, pages 156-170, 2005. · Zbl 1134.68351
[53] Rajeev Motwani and Prabhakar Raghavan.Randomized Algorithms. CUP, New York, NY, USA, 1995. · Zbl 0849.68039
[54] Agust´ın Mista, Alejandro Russo, and John Hughes. Branching processes for quickcheck generators. CoRR, abs/1808.01520, 2018.
[55] C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. InLICS 2006, pages 81-90. IEEE Computer Society Press, 2006.
[56] Pawel Parys. Recursion schemes and the WMSO+U logic. InSTACS 2018, volume 96 ofLIPIcs, pages 53:1-53:16, 2018. · Zbl 1491.03010
[57] Simon M. Poulding and Robert Feldt. Automated random testing in multiple dispatch languages. InICST 2017, pages 333-344. IEEE Computer Society, 2017.
[58] Steven Ramsay, Robin Neatherway, and C.-H. Luke Ong. An abstraction refinement approach to higher-order model checking. InPOPL 2014, pages 61-72. ACM, 2014. · Zbl 1284.68414
[59] N. Saheb-Djahromi. Probabilistic LCF. In J´ozef Winkowski, editor,MFCS 1978, volume 64 of LNCS, pages 442-451. Springer, 1978. · Zbl 0396.68037
[60] Eugene S. Santos. Probabilistic Turing machines and computability.Proc. of the AMS, 22(3):704- 710, 1969. · Zbl 0186.01202
[61] Richard Statman. On the lambdaYcalculus.APAL, 130(1-3):325-337, 2004. · Zbl 1068.03013
[62] Davide Sangiorgi and Valeria Vignudelli. Environmental bisimulations for probabilistic higherorder languages. InPOPL 2016, pages 595-607, 2016. · Zbl 1347.68056
[63] Sylvain Salvati and Igor Walukiewicz. Krivine machines and higher-order schemes. InICALP 2011, volume 6756 ofLNCS, pages 162-173. Springer, 2011. · Zbl 1333.68111
[64] Takeshi Tsukada and C.-H. Luke Ong. Compositional higher-order model checking viaω-regular games over B¨ohm trees. InCSL-LICS 2014, pages 78:1-78:10. ACM, 2014. · Zbl 1401.68207
[65] Frank Wood, Jan Willem Meent, and Vikash Mansinghka. A new approach to probabilistic programming inference. In Samuel Kaski and Jukka Corander, editors,Int. Conf. on Artificial Intelligence and Statistics, volume 33 ofProc. of Machine Learning Research, pages 1024-1032, Reykjavik, Iceland, 22-25 Apr 2014. PMLR.
[66] Mihalis Yannakakis and Kousha Etessami. Checking LTL properties of recursive Markov chains. InQEST 2005, pages 155-165. IEEE Computer Society, 2005.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.