"Black-Box" Probabilistic Verification

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 01, 2004
Accession Number
ADA458539

Entities

People

  • Hakan L. Younes

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Accuracy
  • Algorithms
  • Binomials
  • Computer Science
  • Computers
  • Digital Computers
  • Markov Chains
  • Markov Processes
  • New York
  • Probabilistic Models
  • Probability
  • Probability Distributions
  • Quality Control
  • Random Variables
  • Software Development
  • Stochastic Processes
  • Verification

Fields of Study

  • Computer science

Readers

  • Database Systems and Applications
  • Mathematical Modeling and Probability Theory.

Technology Areas

  • AI & ML
  • AI & ML - Machine Learning Algorithms