Accession Number:

ADA461346

Title:

Model Checking of Probabilistic and Nondeterministic Systems

Descriptive Note:

Corporate Author:

STANFORD UNIV CA

Personal Author(s):

Report Date:

1995-01-01

Pagination or Media Count:

16.0

Abstract:

The temporal logics pCTL and pCTL have been proposed as tools for the formal specification and verification of probabilistic systems as they can express quantitative bounds on the probability of system evolution, they can be used to specify system properties such as reliability and performance. In this paper, we present model-checking algorithms for extensions of pCTL and pCTL to systems in which the probabilistic behavior coexists with nondeterminism, and show that these algorithms have polynomial-time complexity in the size of the system. this provides a practical tool for reasoning on the reliability and performance of parallel systems.

Subject Categories:

  • Statistics and Probability
  • Cybernetics

Distribution Statement:

APPROVED FOR PUBLIC RELEASE