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/
Go to the corresponding LIPIcs Volume Portal

Kattenbelt, Mark ; Huth, Michael

Verification and Refutation of Probabilistic Specifications via Games

pdf-format:
09005.KattenbeltMark.2323.pdf (0.3 MB)

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

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI