Calculating the probability of an LTL formula over a labeled Markov chain

This thesis presents a new algorithm to compute the probability that a state in a labeled Markov chain model satisfies an LTL specification. A solution to this problem was given by Courcoubetis & Yannakakis in 1995, but unlike their solution the algorithm presented here requires no transformations of the input model. This advantage may be significant because of the large models which occur in most practical verification problems. The new algorithm is proved correct and shown to be not worse than doubly exponential in the size of the formula and cubic in the size of the model. However limited experimental results suggest that these bounds are pessimistic and that with further optimization the algorithm might approach the efficiency of current model checkers, which compute only true or false rather than an exact probability. I also include a working Java implementation, MCMC, and a proof that for any plausible path P followed by a Markov chain and any LTL formula Φ, some finite prefix of P determines whether P satisfies Φ