Accession Number:

ADA458539

Title:

"Black-Box" Probabilistic Verification

Descriptive Note:

Research paper

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

2004-09-01

Pagination or Media Count:

18.0

Abstract:

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.

Subject Categories:

  • Theoretical Mathematics
  • Statistics and Probability
  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE