Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Fixed Point Certificates for Reachability and Expected Rewards in MDPs

Krishnendu Chatterjee, Tim Quatmann, Maximilian Schäffeler, Maximilian Weininger, Tobias Winkler, Daniel Zilken

TL;DR

Novel certificates for model checking of Markov decision processes (MDPs) with quantitative reachability and expected reward properties are developed and augment existing algorithms in the probabilistic model checker Storm with the ability to produce certificates.

Abstract

The possibility of errors in human-engineered formal verification software, such as model checkers, poses a serious threat to the purpose of these tools. An established approach to mitigate this problem are certificates -- lightweight, easy-to-check proofs of the verification results. In this paper, we develop novel certificates for model checking of Markov decision processes (MDPs) with quantitative reachability and expected reward properties. Our approach is conceptually simple and relies almost exclusively on elementary fixed point theory. Our certificates work for arbitrary finite MDPs and can be readily computed with little overhead using standard algorithms. We formalize the soundness of our certificates in Isabelle/HOL and provide a formally verified certificate checker. Moreover, we augment existing algorithms in the probabilistic model checker Storm with the ability to produce certificates and demonstrate practical applicability by conducting the first formal certification of the reference results in the Quantitative Verification Benchmark Set.

Fixed Point Certificates for Reachability and Expected Rewards in MDPs

TL;DR

Novel certificates for model checking of Markov decision processes (MDPs) with quantitative reachability and expected reward properties are developed and augment existing algorithms in the probabilistic model checker Storm with the ability to produce certificates.

Abstract

The possibility of errors in human-engineered formal verification software, such as model checkers, poses a serious threat to the purpose of these tools. An established approach to mitigate this problem are certificates -- lightweight, easy-to-check proofs of the verification results. In this paper, we develop novel certificates for model checking of Markov decision processes (MDPs) with quantitative reachability and expected reward properties. Our approach is conceptually simple and relies almost exclusively on elementary fixed point theory. Our certificates work for arbitrary finite MDPs and can be readily computed with little overhead using standard algorithms. We formalize the soundness of our certificates in Isabelle/HOL and provide a formally verified certificate checker. Moreover, we augment existing algorithms in the probabilistic model checker Storm with the ability to produce certificates and demonstrate practical applicability by conducting the first formal certification of the reference results in the Quantitative Verification Benchmark Set.
Paper Structure (62 sections, 46 theorems, 55 equations, 6 figures, 2 tables, 2 algorithms)

This paper contains 62 sections, 46 theorems, 55 equations, 6 figures, 2 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Reachability and Expected Rewards.
  4. Fixed Point Theory.
  5. Certifying Qualitative Reachability
  6. Certificates for Quantitative Reachability
  7. Upper Bounds on Optimal Reachability Probabilities
  8. Lower Bounds on Minimal Reachability Probabilities
  9. Lower Bounds on Maximal Reachability Probabilities
  10. Certificates with an Explicit Witness Strategy.
  11. Certificates without a Witness Strategy.
  12. Certificates for Expected Rewards
  13. Lower Bounds on Optimal Expected Rewards
  14. Upper Bounds on Maximal Expected Rewards
  15. Upper Bounds on Minimal Expected Rewards
  16. ...and 47 more sections

Key Result

theorem 1

Let $(X, \preceq)$ be a complete lattice and $\mathcal{F} \colon X \to X$ be monotone. Then, the set of fixed points$(\{a \in X \mid \mathcal{F}(a) = a\}, \preceq)$ is also a complete lattice. In particular, $\mathcal{F}$ has a least and a greatest fixed point given by $\operatorname{lfp}{\mathcal{F

Figures (6)

  • Figure 1: An MDP with states $S = \{z,s,t\}$, two actions (distinguished by solid and dashed edges), uniform probabilities, and target set $T = \{t\}$. The annotations above and below each state are a certificate for upper and lower bounds on $\mathbb{P}^{\min}(\lozenge T)$, resp.
  • Figure 2: A DTMC.
  • Figure 3: RQ1: Runtime for computing certificates of PI$^X$ and several combinations of mitigation techniques with II (left); and detailed comparison of PI$^X$ and II$^{\ifstrempty{0.05}{}{\circlearrowright 0.05}}_{\mathrm{rnd}}$ (right).
  • Figure 4: RQ2: Runtime overhead of certified MDP model checking for PI$^X$ (left) and II (middle), and scalability of both with respect to the number of states (right).
  • Figure 5: RQ3: Runtime overhead of the certified pipeline/Runtime of certificate checking
  • ...and 1 more figures

Theorems & Definitions (79)

  • theorem 1: Knaster-Tarski
  • definition 1: Distance Operator
  • lemma 1: Unique Fixed Point
  • lemma 2
  • proposition 1: Certificates for $\propt(\reach\target) \!>\! 0$
  • remark 1: Certificates for $\mathbb{P}^{\operatorname{opt}}(\lozenge T) \!=\! 0$
  • definition 2: Complementary Distance Operator
  • lemma 3
  • proposition 2: Certificates for $\propt(\reach\target) \!<\! 1$
  • remark 2: Certificates for $\mathbb{P}^{\operatorname{opt}}(\lozenge T) \!=\! 1$
  • ...and 69 more