Scenario-Based Verification of Uncertain MDPs
295
we instantiate the parameters u ∈ V D by sampling the probability distribution
P. Then, for a given violation probability ν ∈ (0, 1), we compute a solution that
violates the constraints in the LP L r (V D ) with a probability that is not larger
than ν. We first give some properties of the LP L r (U).
Theorem 1. Let uMC D and the sample sets U ⊆ V D with K = |U| ≥ 2. Assume
for all u ∈ U, D[u] |= ϕ r . For a given tolerance probability ν ∈ [0, 1), let the
associated confidence probability
α ν =
1
i=0
K
i
(1 − ν)
K−i ν
i .
(7)
Then, with a probability of at least 1 − α ν , we have
F (D P , ϕ r ) ≥ 1 − ν.
(8)
Proof. The key idea of the proof is to relate the finite LP L r (U ) induced by a
sampled set U to the semi-infinite LP L r (V D ). Then, we use the results given
in [16, Theorem 1] to obtain the lower bound 1 − α ν . Let the convex set C
D P
U (λ, τ )
be generated by the set U according to the probability distribution P over V D as
C
D P
U (λ, τ ) = {(λ, τ ) | ∀u ∈ U satisfying (2) − (6)}.
()
The convex set C
D P
U (λ, τ ) constitutes the set of feasible instantiations to the
LP L r (U ) and is exactly in the form of Equation 5 in [16]. Using C
D P
U (λ, τ ), we
reformulate L r (U ) as the convex program
minimize τ
subject to (λ, τ ) ∈ C
D P
U (λ, τ ),
(9)
where the last constraint denotes that for a given (λ, τ ), the feasible set of
C
D P
U (λ, τ ) is not empty, i.e., there exists a feasible solution pair (λ, τ ) to the
scenario problem L r (U ). This convex program asserts that all MCs in U should
induce a reachability probability that is less than τ , satisfying the specification
ϕ r . Moreover, the convex program constitutes a scenario approximation to the socalled chance-constrained problem [1]. Such an optimization problem states that
the probability of satisfying a (chance) constraint is above a certain threshold:
minimize τ
subject to (λ, τ ) ∈ R × R,
P
(λ, τ ) ∈ C
D P
V D
(λ, τ )
≥ 1 − ν.
(10)
The chance constraint in (10) ensures that the probability that an instantiation—
obtained via distribution P—satisfies the specification ϕ r is at least 1−ν. Theorem
1 in [16] shows that any feasible solution to the problem in (9) is feasible to the
problem in (10) with a confidence probability of 1 − α ν , which shows that the
violation probability of the solution is at most ν. In our case, the probability of
violation is exactly the probability that the instantiated MCs do not satisfy the
specification ϕ r . Thus, the claim follows.
295
we instantiate the parameters u ∈ V D by sampling the probability distribution
P. Then, for a given violation probability ν ∈ (0, 1), we compute a solution that
violates the constraints in the LP L r (V D ) with a probability that is not larger
than ν. We first give some properties of the LP L r (U).
Theorem 1. Let uMC D and the sample sets U ⊆ V D with K = |U| ≥ 2. Assume
for all u ∈ U, D[u] |= ϕ r . For a given tolerance probability ν ∈ [0, 1), let the
associated confidence probability
α ν =
1
i=0
K
i
(1 − ν)
K−i ν
i .
(7)
Then, with a probability of at least 1 − α ν , we have
F (D P , ϕ r ) ≥ 1 − ν.
(8)
Proof. The key idea of the proof is to relate the finite LP L r (U ) induced by a
sampled set U to the semi-infinite LP L r (V D ). Then, we use the results given
in [16, Theorem 1] to obtain the lower bound 1 − α ν . Let the convex set C
D P
U (λ, τ )
be generated by the set U according to the probability distribution P over V D as
C
D P
U (λ, τ ) = {(λ, τ ) | ∀u ∈ U satisfying (2) − (6)}.
()
The convex set C
D P
U (λ, τ ) constitutes the set of feasible instantiations to the
LP L r (U ) and is exactly in the form of Equation 5 in [16]. Using C
D P
U (λ, τ ), we
reformulate L r (U ) as the convex program
minimize τ
subject to (λ, τ ) ∈ C
D P
U (λ, τ ),
(9)
where the last constraint denotes that for a given (λ, τ ), the feasible set of
C
D P
U (λ, τ ) is not empty, i.e., there exists a feasible solution pair (λ, τ ) to the
scenario problem L r (U ). This convex program asserts that all MCs in U should
induce a reachability probability that is less than τ , satisfying the specification
ϕ r . Moreover, the convex program constitutes a scenario approximation to the socalled chance-constrained problem [1]. Such an optimization problem states that
the probability of satisfying a (chance) constraint is above a certain threshold:
minimize τ
subject to (λ, τ ) ∈ R × R,
P
(λ, τ ) ∈ C
D P
V D
(λ, τ )
≥ 1 − ν.
(10)
The chance constraint in (10) ensures that the probability that an instantiation—
obtained via distribution P—satisfies the specification ϕ r is at least 1−ν. Theorem
1 in [16] shows that any feasible solution to the problem in (9) is feasible to the
problem in (10) with a confidence probability of 1 − α ν , which shows that the
violation probability of the solution is at most ν. In our case, the probability of
violation is exactly the probability that the instantiated MCs do not satisfy the
specification ϕ r . Thus, the claim follows.