Title: PCTL Model Checking of Markov Chains: Truth and Falsity as Winning Strategies in Games


Michael Huth  (Imperial College)

Abstract:

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 don't 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
doesn't 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 Buechi type acceptance conditions where simpler fairness conditions
are shown not be to sufficient. Verifier can always force finite plays for certain PCTL
formulae, suggesting the existence of finite-state abstractions of models that satisfy
such formulae.

(Joint work with Harald Fecher, Nir Piterman, and
Daniel Wagner.)