THE COMPLEXITY OF PROBABILISTIC VERIFICATION

We determine the complexity of testing whether a finite state, sequent ial or concurrent probabilistic program satisfies its specification ex pressed in linear-time temporal logic. For sequential programs, we pre sent an algorithm that runs in time linear in the program and exponent ial 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 doubl y exponential in the specification, and prove that it is complete for double exponential time. We also address these questions for specifica tions described by omega-automata or formulas in extended temporal log ic.