Probabilistic verification for "black-box" systems

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. 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. © Springer-Verlag Berlin Heidelberg 2005.