Hintikka Games for PCTL on Labeled Markov Chains

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 B¨uchi 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.

• Type: Conference
• Year: 2008
• Where: QEST
• Authors: Harald Fecher, Michael Huth, Nir Piterman, Daniel Wagner
• Keywords: Countable Labeled Markov, PCTL Formula, QEST 2008, Quantitative Evaluation Of Systems, Strong Until Formulae