Journal of the ACM Bibliography

Costas Courcoubetis and Mihalis Yannakakis. The complexity of probabilistic verification. Journal of the ACM, 42(4):857-907, July 1995. [BibTeX entry]

We determine the complexity of testing whether a finite state, sequential or concurrent probabilistic program satisfies its specification expressed in linear time temporal logic. For sequential programs we present an algorithm that runs in time linear in the program and exponential in the specification, and also show that the problem is in PSPACE, matching the known lower bound. For concurrent programs we show that the problem can be solved in time polynomial in the program and doubly exponential in the specification, and prove that it is complete for double exponential time. We also address these questions for specifications described by omega-automata or formulas in extended temporal logic. Copyright 1995 by ACM, Inc.

The abstract is also available as a LaTeX file, a DVI file, or a PostScript file.

Categories and Subject Descriptors: D.2.4 [Software Engineering]: Program Verification; F.2.2 [Analysis of Algorithms and Problem Complexity]: Nonnumerical Algorithms and Problems -- complexity of proof procedures; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs -- mechanical verification; G.3 [Probability and Statistics] -- probabilistic algorithms

General Terms: Algorithms, Theory, Verification

Additional Key Words and Phrases: Automata, EXPTIME-complete, Markov chain, model checking, probabilistic algorithm, PSPACE-complete, temporal logic

Selected references


  • Journal of the ACM homepage
  • Bibliography top level
  • Journal of the ACM Author Index
  • Search the HBP database