"Black-Box" Probabilistic Verification
CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
Pagination or Media Count:
The authors 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. They present a general model of stochastic discrete event systems that encompasses both discrete-time and continuous-time processes, and also provide a semantics for PCTL interpreted over this model. Their presentation is both a generalization of, and an improvement over, some recent work by Sen et al. on probabilistic verification of black-box systems.
- Theoretical Mathematics
- Statistics and Probability
- Computer Programming and Software