CMU-CS-04-162
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-04-162

"Black-Box" Probabilistic Verification

Håkan L. S. Younes

September 2004

CMU-CS-04-162.ps
CMU-CS-04-162.pdf


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