文章基本信息

标题：Verification and Refutation of Probabilistic Specifications via Games
本地全文：下载
作者：Mark Kattenbelt ; Michael Huth
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2009
卷号：4
页码：251-262
DOI：10.4230/LIPIcs.FSTTCS.2009.2323
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We develop an abstraction-based framework to check probabilistic specifications of Markov Decision Processes (MDPs) using the stochastic two-player game abstractions (\ie ``games'') developed by Kwiatkowska et al.\ as a foundation. We define an abstraction preorder for these game abstractions which enables us to identify many new game abstractions for each MDP --- ranging from compact and imprecise to complex and precise. This added ability to trade precision for efficiency is crucial for scalable software model checking, as precise abstractions are expensive to construct in practice. Furthermore, we develop a four-valued probabilistic computation tree logic (PCTL) semantics for game abstractions. Together, the preorder and PCTL semantics comprise a powerful verification and refutation framework for arbitrary PCTL properties of MDPs.
关键词：Probabilistic model checking; Markov decision processes; Abstraction preorder; Stochastic two-player games