We present Hintikka games for formulae of the probabilistic temporal logic PCTL and countable labeled Markov chains as models, giving an operational account of the denotational semantics of PCTL on such models. Winning strategies have a decent degree of compositionality in the parse tree of a PCTL formula and express the precise evidence for truth or falsity of a PCTL formula. We also prove the existence of monotone winning strategies that are almost finitely representable. Thus this work serves as a foundation for witness and counterexample generation in probabilistic model checking and for a uniform treatment of abstraction-based probabilistic model checking through games.
This work is also of independent interest as it displays a subtle interplay between Buchi acceptance conditions on infinite plays, the strictness or non-strictness of probability thresholds in Strong and Weak Until PCTL formulae in ``GreaterThan'' normal form, and a finite-state approximation lemma for Strong Until formulae with strict thresholds.