288
M. Cubuktepe et al.
Uncertain MDPs. A common approach to deal with unknown system parameters
is to let transition probabilities and cost functions of an MDP belong to uncertainty sets, resulting in so-called uncertain MDPs [25,14,28], which generalize
interval MDPs [20,27,7]. However, solution approaches, e.g., in [25,14,28], usually
rely on the potentially limiting assumption that the uncertainty sets at different
states of the MDP are independent from each other.
Consider a simple motion planning scenario where an unmanned aerial vehicle
(UAV) is tasked to transport a certain payload to a target location. The problem
is to compute a policy for the UAV to successfully deliver the payload while
taking into account the weather conditions. External factors like wind strength
or direction may affect the movement of the UAV. The assumption that such
weather conditions are independent between the different possible states of UAV
is unrealistic, and does not adequately model the scenario at hand.
For settings in which the uncertainties at different states depend on each
other, an option is to account for all possible–albeit infinitely many–values in the
uncertainty sets. The policy synthesis problem can be formulated as a so-called
semi-infinite convex optimization problem, which includes finitely many variables
but infinitely many constraints [28]. This problem, however, is NP-hard [28,18].
Furthermore, it fails to exploit additional information that may be available as
random variables over the uncertainty sets [36], and may be very conservative.
For instance, weather-data in the form of probability distributions may provide
additional information on potential changes during the mission.
In this paper, we study a setting in which the fact the uncertain parameters
are random variables and the dependencies between them are accounted for
explicitly. Furthermore, each random parameter follows an unknown probability
distribution from which we can sample the parameter values.
Problem statement. Compute the probability with which there exists a policy
such that a reachability or an expected-cost specification is satisfied for any
randomly drawn parameter value.
We call this probability the satisfaction probability. The intuition is that the
question of whether all (or some) parameter values satisfy a specification—as
is often done in parameter synthesis [46]—is replaced by the question of how
much we expect the (sampled) model to satisfy a specification. For example, a
satisfaction probability of 80% tells that, if we randomly sample the parameters,
with a probability of 80% there exists a policy for the resulting MDP that satisfies
the specification. Computing the satisfaction probability is in general undecidable,
even for known probability distributions over the parameter values [37].
Scenario-based verification. Therefore, we resort to sampling-based algorithms
that yield a confidence (probability) on the bounds of the satisfaction probability.
Referring back to the UAV example, we want to compute a confidence probability
in the probability that there exists a policy for the UAV to successfully finish the
mission. As a first step, we take the aforementioned semi-infinite optimization
problem that accounts for all possible parameter values as a basis. Each concrete
M. Cubuktepe et al.
Uncertain MDPs. A common approach to deal with unknown system parameters
is to let transition probabilities and cost functions of an MDP belong to uncertainty sets, resulting in so-called uncertain MDPs [25,14,28], which generalize
interval MDPs [20,27,7]. However, solution approaches, e.g., in [25,14,28], usually
rely on the potentially limiting assumption that the uncertainty sets at different
states of the MDP are independent from each other.
Consider a simple motion planning scenario where an unmanned aerial vehicle
(UAV) is tasked to transport a certain payload to a target location. The problem
is to compute a policy for the UAV to successfully deliver the payload while
taking into account the weather conditions. External factors like wind strength
or direction may affect the movement of the UAV. The assumption that such
weather conditions are independent between the different possible states of UAV
is unrealistic, and does not adequately model the scenario at hand.
For settings in which the uncertainties at different states depend on each
other, an option is to account for all possible–albeit infinitely many–values in the
uncertainty sets. The policy synthesis problem can be formulated as a so-called
semi-infinite convex optimization problem, which includes finitely many variables
but infinitely many constraints [28]. This problem, however, is NP-hard [28,18].
Furthermore, it fails to exploit additional information that may be available as
random variables over the uncertainty sets [36], and may be very conservative.
For instance, weather-data in the form of probability distributions may provide
additional information on potential changes during the mission.
In this paper, we study a setting in which the fact the uncertain parameters
are random variables and the dependencies between them are accounted for
explicitly. Furthermore, each random parameter follows an unknown probability
distribution from which we can sample the parameter values.
Problem statement. Compute the probability with which there exists a policy
such that a reachability or an expected-cost specification is satisfied for any
randomly drawn parameter value.
We call this probability the satisfaction probability. The intuition is that the
question of whether all (or some) parameter values satisfy a specification—as
is often done in parameter synthesis [46]—is replaced by the question of how
much we expect the (sampled) model to satisfy a specification. For example, a
satisfaction probability of 80% tells that, if we randomly sample the parameters,
with a probability of 80% there exists a policy for the resulting MDP that satisfies
the specification. Computing the satisfaction probability is in general undecidable,
even for known probability distributions over the parameter values [37].
Scenario-based verification. Therefore, we resort to sampling-based algorithms
that yield a confidence (probability) on the bounds of the satisfaction probability.
Referring back to the UAV example, we want to compute a confidence probability
in the probability that there exists a policy for the UAV to successfully finish the
mission. As a first step, we take the aforementioned semi-infinite optimization
problem that accounts for all possible parameter values as a basis. Each concrete