Scenario-Based Verification of Uncertain MDPs
299
let ν be a violation probability and U the sample set. Then, we can use Theorem 2
or 4 to compute the confidence probability α ν by using the discarding approach
from [19]. Similarly, for a the sample set U and a threshold on the confidence
probability α ν we do a bisection on ν. Specifically, we repeatedly apply Theorem 2
or 4 for different values of ν ∈ (0, 1), to see if the corresponding confidence
probability α ν is below the threshold. We then approximate the lower and upper
bounds on ν.
The correctness of the approach is based on scenario-based optimization.
However, it also applies to an obtained solution by any procedure [39]. For
instance, for any obtained value for the controlled parameters, we can construct
a scenario program by sampling from random parameters. We can then apply
Theorem 2 or 4 to compute the confidence probability α ν or the violation
probability ν.
Generalization to uMDPs. Recall that we want to compute the satisfaction
probability for a uMDP. The probability that for any sampled MDP we are able
to synthesize a policy that satisfies the specification ϕ r . To generalize our results
to uMDPs, we can modify the constraint (6) in the LP L r (U) as
p
u
s ≤
s ∈S
P(s, α, s
)[u] · p
u
s , ∀s ∈ S \ (T ∪ ¬∃♦T ) , ∀α ∈ ActS (s), (20)
asserting that, for each non-target state s ∈ S and action α ∈ ActS (s), the
probability induced by the minimizing policy is an upper bound to the probability
variables p
u
s . The reachability specification ϕ r is satisfied if and only if the
reachability probability at the initial state induced by the minimizing policy is
less than λ. We can assert if ϕ r is satisfied by combining the constraints (20)
with the constraints (2)–(5). Then, our theoretical results apply to the uMDPs.
5 Numerical Examples
We implemented the approach from Section 4 using the model checker Storm [35]
to construct and analyze samples of MDPs. To solve the scenario optimization
problems with cost parameters, we used the SCS solver [31]. All computations
ran on a computer with 8 2.2 GHz cores, and 32 GB of RAM.
We report on a set of well-known benchmarks used in parameter synthesis [46]
that are, for instance, available on the website of the tools PARAM [17] or part
of the PRISM benchmark suite [23]. Moreover, we created a dedicated case study
that is based on the aforementioned UAV example.
5.1 Parameter Synthesis Benchmarks
Setup. In our first set of benchmarks, we adopt parametric MDPs and MCs
from [32]. Essentially, the technique from that paper allows to approximate the
percentage of instantiations that satisfy (or do not satisfy) a specification. We
assume a uniform distribution over the parameter space and set ν equal to the
299
let ν be a violation probability and U the sample set. Then, we can use Theorem 2
or 4 to compute the confidence probability α ν by using the discarding approach
from [19]. Similarly, for a the sample set U and a threshold on the confidence
probability α ν we do a bisection on ν. Specifically, we repeatedly apply Theorem 2
or 4 for different values of ν ∈ (0, 1), to see if the corresponding confidence
probability α ν is below the threshold. We then approximate the lower and upper
bounds on ν.
The correctness of the approach is based on scenario-based optimization.
However, it also applies to an obtained solution by any procedure [39]. For
instance, for any obtained value for the controlled parameters, we can construct
a scenario program by sampling from random parameters. We can then apply
Theorem 2 or 4 to compute the confidence probability α ν or the violation
probability ν.
Generalization to uMDPs. Recall that we want to compute the satisfaction
probability for a uMDP. The probability that for any sampled MDP we are able
to synthesize a policy that satisfies the specification ϕ r . To generalize our results
to uMDPs, we can modify the constraint (6) in the LP L r (U) as
p
u
s ≤
s ∈S
P(s, α, s
)[u] · p
u
s , ∀s ∈ S \ (T ∪ ¬∃♦T ) , ∀α ∈ ActS (s), (20)
asserting that, for each non-target state s ∈ S and action α ∈ ActS (s), the
probability induced by the minimizing policy is an upper bound to the probability
variables p
u
s . The reachability specification ϕ r is satisfied if and only if the
reachability probability at the initial state induced by the minimizing policy is
less than λ. We can assert if ϕ r is satisfied by combining the constraints (20)
with the constraints (2)–(5). Then, our theoretical results apply to the uMDPs.
5 Numerical Examples
We implemented the approach from Section 4 using the model checker Storm [35]
to construct and analyze samples of MDPs. To solve the scenario optimization
problems with cost parameters, we used the SCS solver [31]. All computations
ran on a computer with 8 2.2 GHz cores, and 32 GB of RAM.
We report on a set of well-known benchmarks used in parameter synthesis [46]
that are, for instance, available on the website of the tools PARAM [17] or part
of the PRISM benchmark suite [23]. Moreover, we created a dedicated case study
that is based on the aforementioned UAV example.
5.1 Parameter Synthesis Benchmarks
Setup. In our first set of benchmarks, we adopt parametric MDPs and MCs
from [32]. Essentially, the technique from that paper allows to approximate the
percentage of instantiations that satisfy (or do not satisfy) a specification. We
assume a uniform distribution over the parameter space and set ν equal to the