Probabilistic verification for “black-box” systems

Håkan L. S. Younes


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.

Sample citation

Håkan L. S. Younes. 2005. Probabilistic verification for “black-box” systems. In Proceedings of the 17th International Conference on Computer Aided Verification, edited by Kousha Etessami and Sriram K. Rajamani, vol. 3576 of Lecture Notes in Computer Science, 253–265, Edinburgh, United Kingdom. Springer.

Full paper (13 pages, 15 references)
© Springer-Verlag 2005
Presentation (29 slides)