License
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://drops.dagstuhl.de/opus/volltexte/2009/2323/

Kattenbelt, Mark ; Huth, Michael

Verification and Refutation of Probabilistic Specifications via Games

pdf-format:
Dokument 1.pdf (291 KB)


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 =		{http://dx.doi.org/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
Seminar: 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 Published by LZI