298
M. Cubuktepe et al.
Then, with a probability of at least 1 − α ν , we have F (M P , ϕ c ) ≥ 1 − ν.
Proof. Following the proof of Theorem 1, we define the convex set
C
D P
Uc (κ, τ, c) =
(κ, τ, c) | ∀u ∈ U c such that
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
The main difference compared to the proof of Theorem 1 is that we have
cost parameters in c as the decision variables and we consider an expected cost
specification instead of a reachability specification. Similarly to the proof of
Theorem 1, we reformulate the LP L c (U c ) as the following convex problem
minimize τ
subject to (κ, τ, c) ∈ R × R × R
|W| ,
(κ, τ, c) ∈ C
D P
Uc (κ, τ, c).
(17)
This convex problem is a scenario approximation to the chance constrained
problem given by
minimize τ
subject to (κ, τ, c) ∈ R × R × R
|W| ,
P
(κ, τ, c) ∈ C
D P
V D
(κ, τ, c)
≥ 1 − ν.
(18)
Therefore, similar to the Theorem 1, we obtain the desired claim.
We now consider the case that we compute an instantiation of the cost
variables, and some of the instantiated MCs satisfy the expected cost specification.
We construct the set R c = U c \ Q c , where Q c denotes the set of samples that
induce MCs which violate the specification ϕ c . For this case, we obtain:
Theorem 4. Let uMC D and the sample sets U c , Q c ⊆ V D , with W = |W|,
K = |U c | ≥ 2 and L = |Q|. For a given tolerance probability ν ∈ [0, 1), let the
associated confidence probability
α ν =
l + W + 1
l
l+W +1
i=0
K
i
(1 − ν)
K−i ν
i .
(19)
Then, with a probability of at least 1 − α ν , we have F (M P , ϕ c ) ≥ 1 − ν.
Proof. The proof is similar to the proofs of Theorem 2 and 3, and omitted.
4.4 Building Scenario-Based Algorithms
The question remains how we leverage the theoretical results to compute an
estimate on the satisfaction probability to solve Problems 1 and 2. For instance,
M. Cubuktepe et al.
Then, with a probability of at least 1 − α ν , we have F (M P , ϕ c ) ≥ 1 − ν.
Proof. Following the proof of Theorem 1, we define the convex set
C
D P
Uc (κ, τ, c) =
(κ, τ, c) | ∀u ∈ U c such that
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
The main difference compared to the proof of Theorem 1 is that we have
cost parameters in c as the decision variables and we consider an expected cost
specification instead of a reachability specification. Similarly to the proof of
Theorem 1, we reformulate the LP L c (U c ) as the following convex problem
minimize τ
subject to (κ, τ, c) ∈ R × R × R
|W| ,
(κ, τ, c) ∈ C
D P
Uc (κ, τ, c).
(17)
This convex problem is a scenario approximation to the chance constrained
problem given by
minimize τ
subject to (κ, τ, c) ∈ R × R × R
|W| ,
P
(κ, τ, c) ∈ C
D P
V D
(κ, τ, c)
≥ 1 − ν.
(18)
Therefore, similar to the Theorem 1, we obtain the desired claim.
We now consider the case that we compute an instantiation of the cost
variables, and some of the instantiated MCs satisfy the expected cost specification.
We construct the set R c = U c \ Q c , where Q c denotes the set of samples that
induce MCs which violate the specification ϕ c . For this case, we obtain:
Theorem 4. Let uMC D and the sample sets U c , Q c ⊆ V D , with W = |W|,
K = |U c | ≥ 2 and L = |Q|. For a given tolerance probability ν ∈ [0, 1), let the
associated confidence probability
α ν =
l + W + 1
l
l+W +1
i=0
K
i
(1 − ν)
K−i ν
i .
(19)
Then, with a probability of at least 1 − α ν , we have F (M P , ϕ c ) ≥ 1 − ν.
Proof. The proof is similar to the proofs of Theorem 2 and 3, and omitted.
4.4 Building Scenario-Based Algorithms
The question remains how we leverage the theoretical results to compute an
estimate on the satisfaction probability to solve Problems 1 and 2. For instance,