In this paper, we consider the parameter synthesis problem for parametric Markov decision processes (MDP). Computing the maximal expected value of satisfaction of a logical formula in parametric MDP is a challenging task. Thus, we adopt the scenario approach: instead of computing the precise rational function \(f_{\varphi }\) representing e.g. the maximal expected value, we aim at the approximation function \(\tilde{f}_{\varphi , \lambda }\) that is \(\lambda \) -probably approximately correct with respect to the desired statistical guarantees. The approximation function is based on a template chosen by the user, for instance a polynomial with fixed degree. By means of several theoretical results, we discuss the relation of \(\tilde{f}_{\varphi , \lambda }\) and \(f_{\varphi }\) , and propose a framework for checking properties of the Markov model using \(\tilde{f}_{\varphi , \lambda }\) . An extensive empirical evaluation show the effectiveness of our framework.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

A Scenario Approach for Parametric Markov Decision Processes

  • Zhiming Chi,
  • Ying Liu,
  • Andrea Turrini,
  • Lijun Zhang,
  • David N. Jansen

摘要

In this paper, we consider the parameter synthesis problem for parametric Markov decision processes (MDP). Computing the maximal expected value of satisfaction of a logical formula in parametric MDP is a challenging task. Thus, we adopt the scenario approach: instead of computing the precise rational function \(f_{\varphi }\) representing e.g. the maximal expected value, we aim at the approximation function \(\tilde{f}_{\varphi , \lambda }\) that is \(\lambda \) -probably approximately correct with respect to the desired statistical guarantees. The approximation function is based on a template chosen by the user, for instance a polynomial with fixed degree. By means of several theoretical results, we discuss the relation of \(\tilde{f}_{\varphi , \lambda }\) and \(f_{\varphi }\) , and propose a framework for checking properties of the Markov model using \(\tilde{f}_{\varphi , \lambda }\) . An extensive empirical evaluation show the effectiveness of our framework.