Journal of the Association for Computing Machinery, Vol. 42, No. 4, July 1995, pp. 857–907.

The Complexity of Probabilistic Verification

COSTAS COURCOUBETIS

AND

MIHALIS YANNAKAKIS

Abstract. 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 ω-automata or formulas in extended temporal logic.

Categories and Subject Descriptors. D.2.4; F.2.2 [complexity of proof procedures]; F.3.1 [mechanical verification]; G.3 [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

Copyright 1995 by ACM, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or direct commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or permissions@acm.org.