“Black-box” probabilistic verification

Abstract

We explore the concept of a “black-box” stochastic system, and propose an algorithm for verifying probabilistic properties of such systems based on very weak assumptions regarding system dynamics. The properties are expressed using a variation of PCTL, the Probabilistic Computation Tree Logic. We present a general model of stochastic discrete event systems, which encompasses both discrete-time and continuous-time processes, and we provide a semantics for PCTL interpreted over this model. Our presentation is both a generalization of and an improvement over some recent work by Sen et al. on probabilistic verification of “black-box” systems.

Sample citation

Håkan L. S. Younes. 2004. “Black-box” probabilistic verification. Technical Report CMU-CS-04-162, School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania.

Full paper (17 pages, 17 references)