2016/05/14 by Jansen, Nils, Dehnert, Christian, Kaminski, Benjamin Lucien +2 · 1 citation
#FOS: Computer and information sciences #Programming Languages (cs.PL)
paper · doi:10.48550/arxiv.1605.04477
In this paper we investigate the applicability of standard model checking approaches to verifying properties in probabilistic programming. As the operational model for a standard probabilistic program is a potentially infinite parametric Markov decision process, no direct adaption of existing techniques is possible. Therefore, we propose an on-the-fly approach where the operational model is successively created and verified via a step-wise execution of the program. This approach enables to take key features of many probabilistic programs into account: nondeterminism and conditioning. We discuss the restrictions and demonstrate the scalability on several benchmarks.