Naoki Kobayashi ; Ugo Dal Lago ; Charles Grellois - On the Termination Problem for Probabilistic Higher-Order Recursive Programs

lmcs:5919 - Logical Methods in Computer Science, October 2, 2020, Volume 16, Issue 4 - https://doi.org/10.23638/LMCS-16(4:2)2020
On the Termination Problem for Probabilistic Higher-Order Recursive Programs

Authors: Naoki Kobayashi ; Ugo Dal Lago ORCID-iD; Charles Grellois

    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.


    Volume: Volume 16, Issue 4
    Published on: October 2, 2020
    Accepted on: August 21, 2020
    Submitted on: November 23, 2019
    Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science
    Fundings :
      Source : OpenAIRE Research Graph
    • Expanding Logical Ideas for Complexity Analysis; Funder: French National Research Agency (ANR); Code: ANR-14-CE25-0005
    • Differential Program Semantics; Funder: European Commission; Code: 818616

    Linked data

    Source : ScholeXplorer IsCitedBy ARXIV 2011.14303
    Source : ScholeXplorer IsCitedBy DOI 10.48550/arxiv.2011.14303
    Source : ScholeXplorer IsCitedBy DOI 10.4230/lipics.fscd.2020.19
    Source : ScholeXplorer IsCitedBy DOI 10.46298/lmcs-17(4:15)2021
    • 2011.14303
    • 10.48550/arxiv.2011.14303
    • 10.4230/lipics.fscd.2020.19
    • 10.46298/lmcs-17(4:15)2021
    A Probabilistic Higher-order Fixpoint Logic
    Mitani, Yo ; Kobayashi, Naoki ; Tsukada, Takeshi ;

    Share

    Consultation statistics

    This page has been seen 457 times.
    This article's PDF has been downloaded 268 times.