A Branching-Time Theory for Probabilistic Model-Checking

This paper develops an approach to branching-time probabilistic model checking that is based on quantifying the likelihood with which a system satisfies a formula in the traditional mu-calculus. The semantics uniformly extends the standard interpretation of the mu-calculus and also subsumes work done in more restrictive probabilistic models. We also show how in our setting model checking may be reduced to equation-solving when the system in question is finite-state.