Scenario-Based Verification of Uncertain MDPs
289
parameter value is referred to as a scenario in the convex optimization literature
[15]. For specific problems where a distribution over individual scenarios is
present, a technique called scenario-based optimization provides guarantees on
the satisfaction probability via efficient sampling techniques [15,16]. The basic
idea is to consider a finite set of samples from the distribution over the scenarios
and restrict the semi-infinite problem to these samples. The resulting convex
optimization problem with finitely many constraints can be solved efficiently [50].
For our setting, we first sample a finite number of parameter instantiations
each of which induces a concrete MDP. We can solve the synthesis problem for
this MDP efficiently using, e.g., a probabilistic model checker. Based on the
results, we compute a satisfaction probability and an estimate of its potential
error. For example, a 90% estimate in a satisfaction probability of 80%, means
that the error is at most 10%. We show that the error in the estimate diminishes
to zero exponentially rapidly with increasing number of samples. Moreover, we
show that the number of required samples does neither depend on the size of the
state space nor the number of random parameters. We validate the theoretical
results using several MDPs that have different sizes of state and parameter spaces
and demonstrate experimentally that the required number of samples is indeed
not sensitive to the dimension of the state and parameter space. In addition, we
show the effectiveness of our method with a new dedicated case study based on
the aforementioned UAV example which incorporates 2 500 random parameters.
Related work. The so-called parameter synthesis problem is concerned with
computing parameter values such that there exists a policy in the induced nonparametric MDP that satisfies the specifications. Most of the work in parameter
synthesis focus on finding one parameter value that satisfies the specification.
The approaches involve computing a rational function of the reachability probabilities [11,17,41], utilizing convex optimization [34,40], and sampling-based
methods [26,29]. The problem of whether there exists a value in the parameter
space that satisfies a reachability specification is ETR-complete
4 [47], and finding
a satisfying parameter value is exponential in the number of parameters.
The work in [45] considers the analysis of Markov models in the presence of
uncertain rewards, utilizing statistical methods to reason about the probability
of a parametric MDP satisfying an expected cost specification. This approach
is restricted to reward parameters and does not explicitly compute confidence
bounds. [43] computes bounds on the long-run probability of satisfying a specification with probabilistic uncertainty for Markov chains. Other related techniques
include multi-objective model checking to maximize the average performance with
probabilistic uncertainty sets [36], sampling-based methods which minimize the
regret with uncertainty sets [33], and Bayesian reasoning to compute parameter
values that satisfy a metric temporal logic specification on a continuous-time
Markov chain [38]. [37] considers a variant of the problem in this paper where
4 The ETR satisfiability problem is to decide if there exists a satisfying assignment to
the real variables in a Boolean combination of a set of polynomial inequalities. It is
known that NP ⊆ ETR ⊆ PSPACE.
289
parameter value is referred to as a scenario in the convex optimization literature
[15]. For specific problems where a distribution over individual scenarios is
present, a technique called scenario-based optimization provides guarantees on
the satisfaction probability via efficient sampling techniques [15,16]. The basic
idea is to consider a finite set of samples from the distribution over the scenarios
and restrict the semi-infinite problem to these samples. The resulting convex
optimization problem with finitely many constraints can be solved efficiently [50].
For our setting, we first sample a finite number of parameter instantiations
each of which induces a concrete MDP. We can solve the synthesis problem for
this MDP efficiently using, e.g., a probabilistic model checker. Based on the
results, we compute a satisfaction probability and an estimate of its potential
error. For example, a 90% estimate in a satisfaction probability of 80%, means
that the error is at most 10%. We show that the error in the estimate diminishes
to zero exponentially rapidly with increasing number of samples. Moreover, we
show that the number of required samples does neither depend on the size of the
state space nor the number of random parameters. We validate the theoretical
results using several MDPs that have different sizes of state and parameter spaces
and demonstrate experimentally that the required number of samples is indeed
not sensitive to the dimension of the state and parameter space. In addition, we
show the effectiveness of our method with a new dedicated case study based on
the aforementioned UAV example which incorporates 2 500 random parameters.
Related work. The so-called parameter synthesis problem is concerned with
computing parameter values such that there exists a policy in the induced nonparametric MDP that satisfies the specifications. Most of the work in parameter
synthesis focus on finding one parameter value that satisfies the specification.
The approaches involve computing a rational function of the reachability probabilities [11,17,41], utilizing convex optimization [34,40], and sampling-based
methods [26,29]. The problem of whether there exists a value in the parameter
space that satisfies a reachability specification is ETR-complete
4 [47], and finding
a satisfying parameter value is exponential in the number of parameters.
The work in [45] considers the analysis of Markov models in the presence of
uncertain rewards, utilizing statistical methods to reason about the probability
of a parametric MDP satisfying an expected cost specification. This approach
is restricted to reward parameters and does not explicitly compute confidence
bounds. [43] computes bounds on the long-run probability of satisfying a specification with probabilistic uncertainty for Markov chains. Other related techniques
include multi-objective model checking to maximize the average performance with
probabilistic uncertainty sets [36], sampling-based methods which minimize the
regret with uncertainty sets [33], and Bayesian reasoning to compute parameter
values that satisfy a metric temporal logic specification on a continuous-time
Markov chain [38]. [37] considers a variant of the problem in this paper where
4 The ETR satisfiability problem is to decide if there exists a satisfying assignment to
the real variables in a Boolean combination of a set of polynomial inequalities. It is
known that NP ⊆ ETR ⊆ PSPACE.