License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2009.2323
URN: urn:nbn:de:0030-drops-23233
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2009/2323/
Kattenbelt, Mark ;
Huth, Michael
Verification and Refutation of Probabilistic Specifications via Games
Abstract
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.
BibTeX - Entry
@InProceedings{kattenbelt_et_al:LIPIcs:2009:2323,
author = {Mark Kattenbelt and Michael Huth},
title = {{Verification and Refutation of Probabilistic Specifications via Games}},
booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
pages = {251--262},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-13-2},
ISSN = {1868-8969},
year = {2009},
volume = {4},
editor = {Ravi Kannan and K. Narayan Kumar},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2009/2323},
URN = {urn:nbn:de:0030-drops-23233},
doi = {10.4230/LIPIcs.FSTTCS.2009.2323},
annote = {Keywords: Probabilistic model checking, Markov decision processes, Abstraction preorder, Stochastic two-player games }
}
Keywords: |
|
Probabilistic model checking, Markov decision processes, Abstraction preorder, Stochastic two-player games |
Collection: |
|
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science |
Issue Date: |
|
2009 |
Date of publication: |
|
14.12.2009 |