一句话：提出PHORS模型，证明二阶几乎必然终止不可判定，并给出终止概率的不动点刻画与近似算法。
本文研究概率高阶模型检测问题，旨在结合概率系统模型检测与高阶程序验证。作者提出 PHORS（概率高阶递归方案），作为概率高阶程序的模型，也可视为递归马尔可夫链的高阶扩展。随后研究概率终止/可达性问题，证明二阶 PHORS 的几乎必然终止是不可判定的；同时给出 PHORS 终止概率的不动点刻画，并设计了一个可靠但可能不完备的近似计算过程。作者实现了针对二阶 PHORS 的过程，初步实验表明该过程效果良好。
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 that are reported at the end of the article.
@article{paperbot990,
title = {On the Termination Problem for Probabilistic Higher-Order Recursive Programs},
author = {Naoki Kobayashi and Ugo Dal Lago and Charles Grellois},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 4},
year = {2020},
doi = {10.23638/lmcs-16(4:2)2020}
}