Sciweavers

Share
QEST
2008
IEEE

Hintikka Games for PCTL on Labeled Markov Chains

8 years 8 months ago
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.
Harald Fecher, Michael Huth, Nir Piterman, Daniel
Added 01 Jun 2010
Updated 01 Jun 2010
Type Conference
Year 2008
Where QEST
Authors Harald Fecher, Michael Huth, Nir Piterman, Daniel Wagner
Comments (0)
books