Hintikka Games for PCTL on Labeled Markov Chains

We present Hintikka games for formulae of the probabilistic temporal logic PCTL and countable labeled Markovchains 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 counter example generation in probabilistic model checking through games. This work is also of independent interest as it displaysa subtle interplay between Buchi acceptance conditions oninfinite 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.