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 evolutions, 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.
CITATION STYLE
Bianco, A., & de Alfaro, L. (1995). Model checking of probabilistic and nondeterministic systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1026, pp. 499–513). Springer Verlag. https://doi.org/10.1007/3-540-60692-0_70
Mendeley helps you to discover research relevant for your work.