Scenario Approach for Parametric Markov Models

TL;DR

This paper introduces a scenario-based polynomial approximation framework for analyzing parametric Markov models, enabling efficient property checking with high confidence and outperforming existing tools in benchmarks.

Contribution

It presents a novel PAC-based approximation method for parametric Markov models, allowing direct property checking without complex rational function computation.

Findings

The approach produces accurate polynomial approximations with high confidence.

The method outperforms PRISM and Storm in benchmark experiments.

The tool effectively checks PRCTL properties directly from approximations.

Abstract

In this paper, we propose an approximating framework for analyzing parametric Markov models. Instead of computing complex rational functions encoding the reachability probability and the reward values of the parametric model, we exploit the scenario approach to synthesize a relatively simple polynomial approximation. The approximation is probably approximately correct (PAC), meaning that with high confidence, the approximating function is close to the actual function with an allowable error. With the PAC approximations, one can check properties of the parametric Markov models. We show that the scenario approach can also be used to check PRCTL properties directly, without synthesizing the polynomial at first hand. We have implemented our algorithm in a prototype tool and conducted thorough experiments. The experimental results demonstrate that our tool is able to compute polynomials for more benchmarks than state of the art tools such as PRISM and Storm, confirming the efficacy of our PAC-based synthesis.