Bounded Model Checking for Probabilistic Programs

TL;DR

This paper introduces an on-the-fly bounded model checking method for probabilistic programs, enabling verification of properties in models with nondeterminism and conditioning, which are challenging for traditional techniques.

Contribution

The paper proposes a novel step-wise execution approach for verifying probabilistic programs modeled as parametric Markov decision processes.

Findings

Scalable verification demonstrated on several benchmarks.

Effectively handles nondeterminism and conditioning.

Enables application of model checking to complex probabilistic programs.

Abstract

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.