A Scenario Approach for Parametric Markov Decision Processes
摘要
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.