Scenario-Based Verification of Uncertain MDPs
297
The set C
D P
R (λ, τ ) is in the form of the Definition 2.1 in [16]. We reformulate the
LP L r (R) as the convex program
minimize τ
subject to (λ, τ ) ∈ C
D P
R (λ, τ ).
(14)
where the last constraint denotes that the instantiated MCs from the parameter
values of the set R should induce a reachability probability less than τ , and thus,
satisfy the specification ϕ r . The problem in (14) is a scenario approximation to
the problem in (10). Theorem 2.1 in [19] asserts that with a probability of α ν ,
the violation probability of the solution is at most ν, which is the probability
of violating the specification for the next sample. Similar to Theorem 1, the
violation probability ν is the probability that an instantiated MC does not satisfy
the specification ϕ r . Thus, the claim follows.
4.3 Expected Cost Specifications
So far, we have focused on parameters that were uncontrollable, and assumed to
be random. Now, we consider the case where the cost function c is parametric
and the cost parameters are controllable. Therefore, the parameters in the cost
function are now variables that we can optimize over to satisfy an expected cost
specification ϕ c = EC ≤κ (♦G) for the instantiated MCs. Similar to the previous
sections, we assume that we sample a set of instantiations U c from the probability
distribution P over the parameter space V D . In this case, we modify the LP L r (U )
to obtain the following LP, which we denote by L c (U c ),
minimize τ
subject to ∀u ∈ U c ,
c
u
sI ≤ τ,
c
u
sI ≤ κ,
c
u
s = 0 ∀s ∈ G,
c
u
s = c(s) +
s ∈S
P(s, s
)[u] c
u
s
∀s ∈ S \ G,
(15)
where for s ∈ S, c(s) ∈ R
|W|
≥0 is the cost function at state s, |W| is the number of
the cost parameters, and for u ∈ U c , c
k
s gives the expected cost of reaching the
target G of the instantiated MC D[k] at state s. Note that the cost parameters W
are in the LP L c (U c ) as variables for the parametric cost function,. In the scenario
problem (15), we optimize over c(s) and c
k
s to minimize the maximal induced
cost of the instantiated MCs. If c is an affine function, then the optimization
problem L c (U c ) is convex. In this case, the probabilistic properties of the scenario
problem are given by the following theorem.
Theorem 3. Let uMC D and the sample set U c ⊆ V D with W = |W|, and
K = |U c | ≥ W + 1. Assume for all u ∈ U c , D[k] |= ϕ c . For a given tolerance
probability ν ∈ [0, 1), let the associated confidence probability
α ν =
W +1
i=0
K
i
(1 − ν)
K−i ν
i .
(16)
297
The set C
D P
R (λ, τ ) is in the form of the Definition 2.1 in [16]. We reformulate the
LP L r (R) as the convex program
minimize τ
subject to (λ, τ ) ∈ C
D P
R (λ, τ ).
(14)
where the last constraint denotes that the instantiated MCs from the parameter
values of the set R should induce a reachability probability less than τ , and thus,
satisfy the specification ϕ r . The problem in (14) is a scenario approximation to
the problem in (10). Theorem 2.1 in [19] asserts that with a probability of α ν ,
the violation probability of the solution is at most ν, which is the probability
of violating the specification for the next sample. Similar to Theorem 1, the
violation probability ν is the probability that an instantiated MC does not satisfy
the specification ϕ r . Thus, the claim follows.
4.3 Expected Cost Specifications
So far, we have focused on parameters that were uncontrollable, and assumed to
be random. Now, we consider the case where the cost function c is parametric
and the cost parameters are controllable. Therefore, the parameters in the cost
function are now variables that we can optimize over to satisfy an expected cost
specification ϕ c = EC ≤κ (♦G) for the instantiated MCs. Similar to the previous
sections, we assume that we sample a set of instantiations U c from the probability
distribution P over the parameter space V D . In this case, we modify the LP L r (U )
to obtain the following LP, which we denote by L c (U c ),
minimize τ
subject to ∀u ∈ U c ,
c
u
sI ≤ τ,
c
u
sI ≤ κ,
c
u
s = 0 ∀s ∈ G,
c
u
s = c(s) +
s ∈S
P(s, s
)[u] c
u
s
∀s ∈ S \ G,
(15)
where for s ∈ S, c(s) ∈ R
|W|
≥0 is the cost function at state s, |W| is the number of
the cost parameters, and for u ∈ U c , c
k
s gives the expected cost of reaching the
target G of the instantiated MC D[k] at state s. Note that the cost parameters W
are in the LP L c (U c ) as variables for the parametric cost function,. In the scenario
problem (15), we optimize over c(s) and c
k
s to minimize the maximal induced
cost of the instantiated MCs. If c is an affine function, then the optimization
problem L c (U c ) is convex. In this case, the probabilistic properties of the scenario
problem are given by the following theorem.
Theorem 3. Let uMC D and the sample set U c ⊆ V D with W = |W|, and
K = |U c | ≥ W + 1. Assume for all u ∈ U c , D[k] |= ϕ c . For a given tolerance
probability ν ∈ [0, 1), let the associated confidence probability
α ν =
W +1
i=0
K
i
(1 − ν)
K−i ν
i .
(16)