Abstract
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)
|
|
Håkan L. S. Younes | [ Home > Publications ] |
| Last modified: Wed Jun 8 12:40:22 EDT 2005 |