A Branching-Time Theory for Probabilistic Model-Checking
Purushothaman Iyer, Rance Cleaveland, Murali Narasimha · 2000
. 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. 1 Introduction The temporal-logic model-checking problem may be phrased as follows: given a system modeled as a transition system and a requirement formulated in temporal logic, does the system satisfy the formula? In traditional model-checking, system models can contain nondeterminism, and different schools of thought have arisen regarding the interpretation of temporal formulas over such systems. The linear-time view holds systems should be viewed as sets of sequences of states; in other words, the choices are "...