Model Checking of Probabilistic and Nondeterministic Systems
STANFORD UNIV CA
Pagination or Media Count:
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.
- Statistics and Probability