PCTL model checking of Markov chains: Truth and falsity as winning strategies in games

Probabilistic model checking is a technique for verifying whether a model such as a Markov chain satisfies a probabilistic, behavioral property–e.g. “with probability at least 0.999, a device will be elected leader”. Such properties are expressible in probabilistic temporal logics, e.g. PCTL, and efficient algorithms exist for checking whether these formulae are true or false on finite-state models.Alas, these algorithms do not supply diagnostic information for why a probabilistic property does or does not hold in a given model. We provide here complete and rigorous foundations for such diagnostics in the setting of countable labeled Markov chains and PCTL. For each model and PCTL formula, we define a game between a Verifier and a Refuter that is won by Verifier if the formula holds in the model, and won by Refuter if it does not hold. Games are won by exactly one player, through monotone strategies that encode the diagnostic information for truth and falsity (respectively). These games are infinite with Büchi type acceptance conditions where simpler fairness conditions are shown to be not sufficient. Verifier can always force finite plays for certain PCTL formulae, suggesting the existence of finite-state abstractions of models that satisfy such formulae.