Scenario-Based Verification of Uncertain MDPs
293
Example 2. For the UAV motion planning example, consider the question “What
is the probability on a given day such that there exists a policy for the UAV
to successfully finish the mission.” A possible result is, e.g., 0.78 (confidence
probability: 0.99) and 0.81 (confidence probability: 0.95). Then, with a confidence
probability of 0.99, the actual satisfaction probability is indeed greater than 0.78,
and with a (slightly lower) confidence probability of 0.95 it is greater than 0.81.
Such a result shows that it is quite likely that the UAV will finish the mission
successfully with a probability that is at least 81%.
Similar to Problem 1, we also consider expected cost specifications.
Problem 2. Given a uMDP M P = (M, P), and an expected cost specification
ϕ c = EC ≤κ (♦G), a tolerance probability ν, and a confidence probability α ν
determine if there exists an instantiation to the cost parameters such that
F (M P , ϕ c ) ≥ 1 − ν holds with a probability of at least 1 − α ν .
Remark 2. The main difference between Problem 1 and Problem 2 is that we
consider controllable cost parameters. We seek to compute an instantiation to
these parameters such that the satisfaction probability is greater than 1 − ν with
high confidence.
4 Scenario-Based Verification
In this section, we present our approach to solving Problem 1 and 2, that is,
to approximate the satisfaction probability with respect to a specification. We
first consider the robust policy synthesis problem that accounts for all possible
values in the uncertainty set, potentially leading to a very pessimistic result.
This problem can be formulated as a semi-infinite convex optimization problem,
which is NP-hard [28]. Here, we exploit the structure of this problem, which
includes finitely many variables but infinitely many constraints. Our approach is
based on scenario optimization [15,16]: We sample a finite number of parameter
values and restrict the semi-infinite problem to these samples. The resulting
finite-dimensional convex optimization problem can be solved efficiently [50].
Based on the solution of the optimization problem, we compute high confidence
in the estimate of the satisfaction probability. The estimate also generalizes to
the samples from the probability distribution that are not in the sample set.
Remark 3. For ease of presentation, we focus on uncertain Markov chains (uMCs).
Our results and methods generalize to uncertain MDPs (uMDPs).
We first develop the main results for the simple setting where all sampled
instantiated MCs from the parameter space V D satisfy the reachability specification ϕ r . This assumption does not imply that all instantiated MCs satisfy ϕ r :
The sample set does not contain an MC that violates ϕ r even though there exists
such an MC in the parameter space. In Section 4.2, we drop this assumption
and allow sampled points in V D to violate ϕ r . This completes our treatment of
Problem 1. In Section 4.3, we show how our results generalize to expected cost
specifications ϕ c , to solve Problem 2.
293
Example 2. For the UAV motion planning example, consider the question “What
is the probability on a given day such that there exists a policy for the UAV
to successfully finish the mission.” A possible result is, e.g., 0.78 (confidence
probability: 0.99) and 0.81 (confidence probability: 0.95). Then, with a confidence
probability of 0.99, the actual satisfaction probability is indeed greater than 0.78,
and with a (slightly lower) confidence probability of 0.95 it is greater than 0.81.
Such a result shows that it is quite likely that the UAV will finish the mission
successfully with a probability that is at least 81%.
Similar to Problem 1, we also consider expected cost specifications.
Problem 2. Given a uMDP M P = (M, P), and an expected cost specification
ϕ c = EC ≤κ (♦G), a tolerance probability ν, and a confidence probability α ν
determine if there exists an instantiation to the cost parameters such that
F (M P , ϕ c ) ≥ 1 − ν holds with a probability of at least 1 − α ν .
Remark 2. The main difference between Problem 1 and Problem 2 is that we
consider controllable cost parameters. We seek to compute an instantiation to
these parameters such that the satisfaction probability is greater than 1 − ν with
high confidence.
4 Scenario-Based Verification
In this section, we present our approach to solving Problem 1 and 2, that is,
to approximate the satisfaction probability with respect to a specification. We
first consider the robust policy synthesis problem that accounts for all possible
values in the uncertainty set, potentially leading to a very pessimistic result.
This problem can be formulated as a semi-infinite convex optimization problem,
which is NP-hard [28]. Here, we exploit the structure of this problem, which
includes finitely many variables but infinitely many constraints. Our approach is
based on scenario optimization [15,16]: We sample a finite number of parameter
values and restrict the semi-infinite problem to these samples. The resulting
finite-dimensional convex optimization problem can be solved efficiently [50].
Based on the solution of the optimization problem, we compute high confidence
in the estimate of the satisfaction probability. The estimate also generalizes to
the samples from the probability distribution that are not in the sample set.
Remark 3. For ease of presentation, we focus on uncertain Markov chains (uMCs).
Our results and methods generalize to uncertain MDPs (uMDPs).
We first develop the main results for the simple setting where all sampled
instantiated MCs from the parameter space V D satisfy the reachability specification ϕ r . This assumption does not imply that all instantiated MCs satisfy ϕ r :
The sample set does not contain an MC that violates ϕ r even though there exists
such an MC in the parameter space. In Section 4.2, we drop this assumption
and allow sampled points in V D to violate ϕ r . This completes our treatment of
Problem 1. In Section 4.3, we show how our results generalize to expected cost
specifications ϕ c , to solve Problem 2.