292
M. Cubuktepe et al.
s0
start
s1
s2
s3
s4
s5
s6
s7
1 − v
v
0.1 · (1 − v)
1 − v
v + 0.9 · (1 − v)
v
1 − 0.5 · v
2
v
0.5 · v
2
1 − v
1
1
1
0
0.2 0.4 0.6 0.8
1
0
0.05
0.1
λ
0.15
v
P≤λ(♦T )
Fig. 1. Left: A uMC with parameter v. Right: The probability of satisfying the reachability specification ϕr = P ≤λ (♦T ) versus the value of the parameter v. Intervals that
satisfy ϕr are green, intervals that violate ϕr are red.
with u ∈ V M and I ϕ : V M → {0, 1} is the indicator for ϕ, i.e. I ϕ (u) = 1 iff
M[u] |= ϕ.
Note that I ϕ is measurable, as V M is the finite union of semi-algebraic sets [49].
Moreover, we have that F (M P , ϕ) ∈ [0, 1] and F (M P , ϕ) + F (M P , ¬ϕ) = 1.
Example 1. Consider the uMC in the left figure of Fig. 1 with the uncontrollable
parameter set V = {v}, initial state s 0 , target set T = {s 3 } and an uniform
distribution for the parameter v over the interval [0, 1]. We plot the probability of
satisfying the specification ϕ r = P ≤λ (♦T ) as a function of v in the right figure of
Fig. 1. We also show the satisfying region and its complementary as green and red
regions. The satisfying region is given by the union of the intervals [0.13, 0.525]
and [0.89, 1.0], and the satisfaction probability F (M P , ϕ r ) is 0.395 + 0.11 = 0.505.
3 Problem Statement
In this section, we state the problem that we study in this paper. We seek to
compute the satisfaction probability of the parameter space for a reachability or
an expected cost specification ϕ on a uMDP. Intuitively, we seek the probability
that a randomly sampled instantiation from the parameter space induces an MDP
which satisfies ϕ. Formally: Given a uMDP M P = (M, P), and a specification
ϕ, compute the satisfaction probability F (M P , ϕ). However, as mentioned, the
problem is in general undecidable [37]. Therefore, we consider an approximation
of computing the satisfaction probability:
Problem 1. Given a uMDP M P = (M, P), a reachability specification ϕ r =
P ≤λ (♦T ), and a tolerance probability ν, compute a confidence probability
α ν such that F (M P , ϕ r ) ≥ 1 − ν holds with a probability of at least 1 − α ν .
We illustrate the problem statement with the following example.
M. Cubuktepe et al.
s0
start
s1
s2
s3
s4
s5
s6
s7
1 − v
v
0.1 · (1 − v)
1 − v
v + 0.9 · (1 − v)
v
1 − 0.5 · v
2
v
0.5 · v
2
1 − v
1
1
1
0
0.2 0.4 0.6 0.8
1
0
0.05
0.1
λ
0.15
v
P≤λ(♦T )
Fig. 1. Left: A uMC with parameter v. Right: The probability of satisfying the reachability specification ϕr = P ≤λ (♦T ) versus the value of the parameter v. Intervals that
satisfy ϕr are green, intervals that violate ϕr are red.
with u ∈ V M and I ϕ : V M → {0, 1} is the indicator for ϕ, i.e. I ϕ (u) = 1 iff
M[u] |= ϕ.
Note that I ϕ is measurable, as V M is the finite union of semi-algebraic sets [49].
Moreover, we have that F (M P , ϕ) ∈ [0, 1] and F (M P , ϕ) + F (M P , ¬ϕ) = 1.
Example 1. Consider the uMC in the left figure of Fig. 1 with the uncontrollable
parameter set V = {v}, initial state s 0 , target set T = {s 3 } and an uniform
distribution for the parameter v over the interval [0, 1]. We plot the probability of
satisfying the specification ϕ r = P ≤λ (♦T ) as a function of v in the right figure of
Fig. 1. We also show the satisfying region and its complementary as green and red
regions. The satisfying region is given by the union of the intervals [0.13, 0.525]
and [0.89, 1.0], and the satisfaction probability F (M P , ϕ r ) is 0.395 + 0.11 = 0.505.
3 Problem Statement
In this section, we state the problem that we study in this paper. We seek to
compute the satisfaction probability of the parameter space for a reachability or
an expected cost specification ϕ on a uMDP. Intuitively, we seek the probability
that a randomly sampled instantiation from the parameter space induces an MDP
which satisfies ϕ. Formally: Given a uMDP M P = (M, P), and a specification
ϕ, compute the satisfaction probability F (M P , ϕ). However, as mentioned, the
problem is in general undecidable [37]. Therefore, we consider an approximation
of computing the satisfaction probability:
Problem 1. Given a uMDP M P = (M, P), a reachability specification ϕ r =
P ≤λ (♦T ), and a tolerance probability ν, compute a confidence probability
α ν such that F (M P , ϕ r ) ≥ 1 − ν holds with a probability of at least 1 − α ν .
We illustrate the problem statement with the following example.