Model Checking of Probabilistic and Nondeterministic Systems

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1995
Accession Number
ADA461346

Entities

People

  • Andrea Bianco
  • Luca De Alfaro

Organizations

  • Stanford University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Air Force
  • Algorithms
  • Computer Science
  • Computers
  • Contracts
  • Information Operations
  • Reliability
  • Scientific Research
  • Specifications
  • Standards

Fields of Study

  • Computer science
  • Engineering

Readers

  • Mathematical Modeling and Probability Theory.