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 reports@cs.cmu.edu