Hintikka Games for PCTL on Labeled Markov Chains

Michael Huth ( Imperial College, London )

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 through games. This work is also of independent interest as it displays a subtle interplay between Buechi 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. This is joint work with Harald Fecher, Nir Piterman, and Daniel Wagner.