Hintikka Games for PCTL on Labeled Markov Chains
Hintikka Games for PCTL on Labeled Markov Chains
复制标题
标记马尔可夫链上 PCTL 的 Hintikka 游戏
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Daniel Wagner
中科院分区：
文献类型：
--
作者：
Harald Fecher;M. Huth;Nir Piterman;Daniel Wagner
我们提出了Hintikka游戏的概率时序逻辑PCTL和可数标记马尔可夫链作为模型的公式，给出了操作帐户的指称语义的PCTL对这样的模型。获胜策略在PCTL公式的解析树中具有相当程度的组合性，并且表达了PCTL公式的真或假的精确证据。我们还证明了存在的单调获胜的策略，几乎是可表示的。因此，这项工作作为一个基础，证人和反例生成概率模型检测通过游戏。这项工作也是独立的兴趣，因为它显示一个微妙的相互作用之间的Buchi接受条件oninfinite播放，严格或非严格的概率阈值在强和弱直到PCTL公式在“大于”正常形式，和有限状态近似引理强直到公式严格的阈值。
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.