294
M. Cubuktepe et al.
4.1 Restriction to Satisfying Samples
In this section, we assume that all instantiated MCs satisfy ϕ r . We then generalize
our method to any values of ν. We want to check if a uMC D satisfies a reachability
specification ϕ r = P ≤λ (♦T ) for all instantiations in the sample set U . For each
instantiation, we can formulate a linear program (LP) that is feasible if and only
if ϕ r is satisfied [51]. For a subset U ⊆ V D of the parameter space V D of the uMC
D, we can then write the conjunction of these LPs. We assume that |U| is finite
and sampled from the probability distribution P over the parameter space V D .
For each instantiation u ∈ U, we introduce a set of linear constraints that
are parametrized by u
6 . We use the following variables. For s ∈ S and u ∈ U,
the variable p
u
s ∈ [0, 1] represents the probability of reaching the target set
T ⊆ S from state s. The variable τ represents an upper bound on the probability
of satisfying ϕ r for all instantiations in U . Note that τ is a variable in our
formulation, whereas λ is the threshold of the reachability specification, and
thus constant. The set ¬∃♦T represents the set of states which cannot reach the
target set T . The probability of reaching T from these states is zero, and the set
¬∃♦T does not change for different graph-preserving instantiations [17]. The set
¬∃♦T can be found in polynomial time in the size of a uMC by using standard
graph-based search algorithms [48]. We solve the following LP L r (U ), which is
parametrized by each instantiation u in U ,
minimize τ
(1)
subject to ∀u ∈ U,
p
u
sI ≤ τ,
(2)
p
u
sI ≤ λ,
(3)
p
u
s = 1, ∀s ∈ T,
(4)
p
u
s = 0, ∀s ∈ ¬∃♦T,
(5)
p
u
s =
s ∈S
P(s, s
)[u] · p
u
s , ∀s ∈ S \ (T ∪ ¬∃♦T ) .
(6)
The objective (1) minimizes the maximal probability that can be achieved by
all MCs induced by U . The constraint (2) represents an upper bound on the
reachability probability for all instantiations. We minimize the upper bound to
compute the maximal probability of satisfying ϕ r for all instantiated MCs. The
constraint (3) ensures that the probability of reaching T from the initial state s I
is below the threshold λ. The constraint (4) sets the probability to reach a state
in T from T to 1. The constraint (5) sets the reachability probabilities from the
states in ¬∃♦T to zero. The constraint (6) computes the probability of satisfying
the specification for each non-target state s ∈ S in the standard way.
There are infinitely many constraints in the semi-infinite LP L r (V D ) as the
cardinality of (V D ) is infinite and L r (V D ) has infinitely many constraints in the
form of (2)–(6). Our approach is based on scenario optimization [13,15,16], where
6 we assume that each sample has a unique index
M. Cubuktepe et al.
4.1 Restriction to Satisfying Samples
In this section, we assume that all instantiated MCs satisfy ϕ r . We then generalize
our method to any values of ν. We want to check if a uMC D satisfies a reachability
specification ϕ r = P ≤λ (♦T ) for all instantiations in the sample set U . For each
instantiation, we can formulate a linear program (LP) that is feasible if and only
if ϕ r is satisfied [51]. For a subset U ⊆ V D of the parameter space V D of the uMC
D, we can then write the conjunction of these LPs. We assume that |U| is finite
and sampled from the probability distribution P over the parameter space V D .
For each instantiation u ∈ U, we introduce a set of linear constraints that
are parametrized by u
6 . We use the following variables. For s ∈ S and u ∈ U,
the variable p
u
s ∈ [0, 1] represents the probability of reaching the target set
T ⊆ S from state s. The variable τ represents an upper bound on the probability
of satisfying ϕ r for all instantiations in U . Note that τ is a variable in our
formulation, whereas λ is the threshold of the reachability specification, and
thus constant. The set ¬∃♦T represents the set of states which cannot reach the
target set T . The probability of reaching T from these states is zero, and the set
¬∃♦T does not change for different graph-preserving instantiations [17]. The set
¬∃♦T can be found in polynomial time in the size of a uMC by using standard
graph-based search algorithms [48]. We solve the following LP L r (U ), which is
parametrized by each instantiation u in U ,
minimize τ
(1)
subject to ∀u ∈ U,
p
u
sI ≤ τ,
(2)
p
u
sI ≤ λ,
(3)
p
u
s = 1, ∀s ∈ T,
(4)
p
u
s = 0, ∀s ∈ ¬∃♦T,
(5)
p
u
s =
s ∈S
P(s, s
)[u] · p
u
s , ∀s ∈ S \ (T ∪ ¬∃♦T ) .
(6)
The objective (1) minimizes the maximal probability that can be achieved by
all MCs induced by U . The constraint (2) represents an upper bound on the
reachability probability for all instantiations. We minimize the upper bound to
compute the maximal probability of satisfying ϕ r for all instantiated MCs. The
constraint (3) ensures that the probability of reaching T from the initial state s I
is below the threshold λ. The constraint (4) sets the probability to reach a state
in T from T to 1. The constraint (5) sets the reachability probabilities from the
states in ¬∃♦T to zero. The constraint (6) computes the probability of satisfying
the specification for each non-target state s ∈ S in the standard way.
There are infinitely many constraints in the semi-infinite LP L r (V D ) as the
cardinality of (V D ) is infinite and L r (V D ) has infinitely many constraints in the
form of (2)–(6). Our approach is based on scenario optimization [13,15,16], where
6 we assume that each sample has a unique index