Model Checking of Probabilistic and Nondeterministic Systems

Publisher Website
Google Scholar
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.

This publication has 0 references indexed in Scilit: