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 higherorder probabilistic programming languages, not much has been done to combine those two approaches. As a first step towards model checking of probabilistic higher-order programs, we introduce PHORS, a probabilistic extension of higher-order recursion schemes (HORS), as a model of probabilistic higherorder 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.
On the termination problem for probabilistic higher-order recursive programs / Kobayashi N.; Dal Lago U.; Grellois C.. - ELETTRONICO. - 2019-:(2019), pp. 8785679.1-8785679.12. (Intervento presentato al convegno 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019 tenutosi a SFU Harbour Centre in Downtown Vancouver, can nel 2019) [10.1109/LICS.2019.8785679].
On the termination problem for probabilistic higher-order recursive programs
Dal Lago U.
;
2019
Abstract
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 higherorder probabilistic programming languages, not much has been done to combine those two approaches. As a first step towards model checking of probabilistic higher-order programs, we introduce PHORS, a probabilistic extension of higher-order recursion schemes (HORS), as a model of probabilistic higherorder 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.File | Dimensione | Formato | |
---|---|---|---|
1811.02133.pdf
accesso aperto
Tipo:
Postprint
Licenza:
Licenza per Accesso Aperto. Creative Commons Attribuzione (CCBY)
Dimensione
861.9 kB
Formato
Adobe PDF
|
861.9 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.