On the Termination Problem for Probabilistic Higher-Order Recursive Programs

摘要

In the last two decades, there has been much progress on model checking ofboth probabilistic systems and higher-order programs. In spite of the emergenceof higher-order probabilistic programming languages, not much has been done tocombine those two approaches. In this paper, we initiate a study on theprobabilistic higher-order model checking problem, by giving some firsttheoretical and experimental results. As a first step towards our goal, weintroduce PHORS, a probabilistic extension of higher-order recursion schemes(HORS), as a model of probabilistic higher-order programs. The model of PHORSmay alternatively be viewed as a higher-order extension of recursive Markovchains. We then investigate the probabilistic termination problem -- or,equivalently, the probabilistic reachability problem. We prove that almost suretermination of order-2 PHORS is undecidable. We also provide a fixpointcharacterization of the termination probability of PHORS, and develop a sound(but possibly incomplete) procedure for approximately computing the terminationprobability. We have implemented the procedure for order-2 PHORSs, andconfirmed that the procedure works well through preliminary experiments thatare reported at the end of the article.