296
M. Cubuktepe et al.
Remark 4 (Independence to model size). The confidence probability in Theorem 1 is in fact independent from the number of states, transitions, or random
parameters of the uMC. From a practical perspective, the number of samples
that are needed for a certain confidence does not depend on the model size.
Finally, Theorem 1 asserts that with a probability of at least 1 − α ν , the next
sampled point from V D will satisfy the specification with a probability of at least
1 − ν. Note that α ν is the tail probability of a binomial distribution. It converges
exponentially rapidly to 0 in |U| [16].
4.2 Satisfaction Probability by Treating Violating Samples
Theorem 1 assumes that all sampled points, that is, the induced MCs, satisfy the
specification ϕ r . This is a severe assumption in general. To lift this assumption,
we consider the discarding approach from [19]. Specifically, after sampling a set of
instantiations U from V D according to the probability distribution P, we remove
the constraints for the MCs that violate the specification ϕ r from the LP. We
construct the set R = U \Q, where Q denotes the set of samples that induce MCs
violating the specification ϕ r . Therefore, the set R denotes the set of sampled
MCs that satisfy the specification ϕ r . We then solve the LP L r (R)
minimize τ
subject to ∀u ∈ R,
(2) − (6),
(11)
where for u ∈ R and s ∈ S, p
u
s gives the probability of satisfying the reachability
specification of the instantiated MC D[u] at state s. The other constraints in the
optimization problem in LP L r (R) are identical to the LP L r (U ). We give the
main result of this section.
Theorem 2. Let uMC D and the sample sets U, Q ⊆ V D , with K = |U| ≥ 2 and
L = |Q|. For a given tolerance probability ν ∈ [0, 1), the associated confidence
probability is
α ν =
L + 1
L
L+1
i=0
K
i
(1 − ν)
K−i ν
i .
(12)
Then, with a probability of at least 1 − α ν , we have
F (D P , ϕ r ) ≥ 1 − ν.
(13)
Proof. Similar to the proof of Theorem 1, the main idea is to relate the LP L r (R)
to the chance-constrained convex problem in (10). Then, we invoke the results
from [19, Theorem 1] to get the desired result. Let the convex set C
D P
R (λ, τ ),
which is generated by the samples in R, be defined by
C
D P
R (λ, τ ) = {(λ, τ ) | ∀u ∈ R such that (∗) is satisfied}.
M. Cubuktepe et al.
Remark 4 (Independence to model size). The confidence probability in Theorem 1 is in fact independent from the number of states, transitions, or random
parameters of the uMC. From a practical perspective, the number of samples
that are needed for a certain confidence does not depend on the model size.
Finally, Theorem 1 asserts that with a probability of at least 1 − α ν , the next
sampled point from V D will satisfy the specification with a probability of at least
1 − ν. Note that α ν is the tail probability of a binomial distribution. It converges
exponentially rapidly to 0 in |U| [16].
4.2 Satisfaction Probability by Treating Violating Samples
Theorem 1 assumes that all sampled points, that is, the induced MCs, satisfy the
specification ϕ r . This is a severe assumption in general. To lift this assumption,
we consider the discarding approach from [19]. Specifically, after sampling a set of
instantiations U from V D according to the probability distribution P, we remove
the constraints for the MCs that violate the specification ϕ r from the LP. We
construct the set R = U \Q, where Q denotes the set of samples that induce MCs
violating the specification ϕ r . Therefore, the set R denotes the set of sampled
MCs that satisfy the specification ϕ r . We then solve the LP L r (R)
minimize τ
subject to ∀u ∈ R,
(2) − (6),
(11)
where for u ∈ R and s ∈ S, p
u
s gives the probability of satisfying the reachability
specification of the instantiated MC D[u] at state s. The other constraints in the
optimization problem in LP L r (R) are identical to the LP L r (U ). We give the
main result of this section.
Theorem 2. Let uMC D and the sample sets U, Q ⊆ V D , with K = |U| ≥ 2 and
L = |Q|. For a given tolerance probability ν ∈ [0, 1), the associated confidence
probability is
α ν =
L + 1
L
L+1
i=0
K
i
(1 − ν)
K−i ν
i .
(12)
Then, with a probability of at least 1 − α ν , we have
F (D P , ϕ r ) ≥ 1 − ν.
(13)
Proof. Similar to the proof of Theorem 1, the main idea is to relate the LP L r (R)
to the chance-constrained convex problem in (10). Then, we invoke the results
from [19, Theorem 1] to get the desired result. Let the convex set C
D P
R (λ, τ ),
which is generated by the samples in R, be defined by
C
D P
R (λ, τ ) = {(λ, τ ) | ∀u ∈ R such that (∗) is satisfied}.