“Black-Box” Probabilistic Verification

Håkan L. S. Younes

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.

Full paper: PDF, PS (17 pages, 17 references)

Valid XHTML 1.0! Håkan L. S. Younes Home > Publications ]
Last modified: Wed Jun 8 12:40:22 EDT 2005