Probabilistic verification for ``black-box'' 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. Properties are expressed as formulae in a probabilistic temporal logic. Our presentation is a generalization of and an improvement over recent work by Sen et al. on probabilistic verification for ``black-box'' systems.