Hintikka Games for PCTL on Labeled Markov Chains

We present Hintikka games for formulae of the proba-bilistic temporal logic PCTL and countable labeled Markov chains as models, giving an operational account of the de-notational 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 evi-dence 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 Büchi acceptance conditions on infinite plays, the strictness or non-strictness of probabil-ity thresholds in Strong and Weak Until PCTL formulae in “GreaterThan ” normal form, and a finite-state approxima-tion lemma for Strong Until formulae with strict thresholds