Verification and Refutation of Probabilistic Specifications via Games

Kattenbelt, Mark; Huth, Michael

doi:10.4230/LIPIcs.FSTTCS.2009.2323

Document

Verification and Refutation of Probabilistic Specifications via Games

Authors Mark Kattenbelt, Michael Huth

Part of: Volume: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2009)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)
License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
Publication Date: 2009-12-14

PDF

File

PDF

LIPIcs.FSTTCS.2009.2323.pdf

Filesize: 291 kB
12 pages

Document Identifiers

DOI: 10.4230/LIPIcs.FSTTCS.2009.2323
URN: urn:nbn:de:0030-drops-23233

Subject Classification

Keywords

Probabilistic model checking
Markov decision processes
Abstraction preorder
Stochastic two-player games

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

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.

Cite As Get BibTex

Mark Kattenbelt and Michael Huth. Verification and Refutation of Probabilistic Specifications via Games. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 251-262, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009) https://doi.org/10.4230/LIPIcs.FSTTCS.2009.2323

Author Details

Mark Kattenbelt

Michael Huth

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail