Computer Science Department
School of Computer Science, Carnegie Mellon University


"Black-Box" Probabilistic Verification

Håkan L. S. Younes

September 2004

Keywords: Probabilistic verification, model checking, temporal logic, statistical hypothesis testing, stochastic processes, discrete event systems

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.

17 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by