%%% ====================================================================
%%%  @LaTeX-file{
%%%     filename  = "courcoubetisy95.ltx",
%%%     date      = "20 November 1995",
%%%     time      = "21:41:36 EST",
%%%     author    = "David M. Jones",
%%%     email     = "jacm@theory.lcs.mit.edu",
%%%     url       = "http://theory.lcs.mit.edu/~jacm/",
%%%     address   = "Journal of the ACM
%%%                  MIT Laboratory for Computer Science
%%%                  Room NE43-316
%%%                  545 Technology Square
%%%                  Cambridge, MA 02139
%%%                  USA",
%%%     telephone = "(617) 253-5936",
%%%     FAX       = "(617) 253-3480",
%%%     checksum  = "63467 104 414 3583",
%%%     codetable = "ISO/ASCII",
%%%     supported = "yes",
%%%     docstring = "Copyright (c) 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.
%%%                  
%%%                  This is a LaTeX2e file.  To process it, you will
%%%                  need a copy of the acmabs document class, which is
%%%                  available via the following URL:
%%%
%%%                  http://theory.lcs.mit.edu/~jacm/acmart/acmabs.cls
%%%                  ",
%%%  }
%%% ====================================================================

\documentclass{acmabs}

\begin{document}

\Journal{Journal of the ACM}

\refkey{CourcoubetisY95}

\title{The Complexity of Probabilistic Verification}

\author{Costas Courcoubetis \and Mihalis Yannakakis}

\Pages{857--907}

\Month{July}

\Year{1995}

\Volume{42}

\Number{4}

\maketitle

\begin{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 $\omega$-automata or formulas in
  extended temporal logic.

\end{abstract}

\begin{categories}

D.2.4; F.2.2 [complexity of proof procedures]; F.3.1 [mechanical verification];
  G.3 [probabilistic algorithms]

\end{categories}

\begin{terms}

Algorithms, Theory, Verification

\end{terms}

\begin{keywords}

Automata, EXPTIME-complete, Markov chain, model checking, probabilistic
  algorithm, PSPACE-complete, temporal logic

\end{keywords}

\end{document}