Scenario-Based Verification of Uncertain MDPs
291
instantiation u is well-defined for M if the resulting model M[u] is an MDP. We
assume that all parameter instantiations in V M yield well-defined MDPs. We call
u graph-preserving if for all s, s
∈ S and α ∈ Act it holds that P(s, α, s
) = 0 ⇒
P(s, α, s
)[u] ∈ (0, 1]. If P(s, α, s
) ∈ {p, 1 − p | p ∈ V } ∪ Q, then the parameter
space V M is given by the rectangle [0, 1]
|V | . We also consider a state-action cost
function c : S × Act → Q[V ]. We denote the set of cost parameters as W.
To define measures on MDPs, nondeterministic choices are resolved by a
so-called policy σ : S → Act with σ(s) ∈ ActS (s). The set of all policies over
M is Str
M . For the specifications that we consider in this paper, memoryless
deterministic policies are sufficient [48]. Applying a policy to an MDP yields an
induced Markov chain where all nondeterminism is resolved.
For an MC D, the reachability specification ϕ r = P ≤λ (♦T ) asserts that a set
T ⊆ S of target states is reached with probability at most λ ∈ [0, 1]
5 . If ϕ r holds
for D, we write D |= ϕ r . Model checking for the more general PCTL [4] or ωregular specifications is often reducible to checking reachability specifications [48].
For an MDP M, ϕ r holds if for all σ ∈ Str
M such that the induced MC D by the
policy σ reaches the set T with a probability of at most λ. For an expected cost
specification ϕ c = EC ≤κ (♦G), it holds that D |= ϕ c if and only if the expected
cost of reaching a set G ⊆ S is at most κ ∈ R. The expected cost of reaching G
is well-defined if and only if P(♦T ) = 1 for all policies in an MDP.
2.2 Uncertain MDPs
We now introduce the setting that we study in this paper. Specifically, we use
parameters to define the uncertainty in the transition probabilities and cost
functions of an MDP. Each random parameter follows an unknown probability
distribution from which we can sample the parameter values.
Definition 2 (uMDP). An uncertain Markov decision process M P (uMDP)
is a tuple M P = (M, P) where M is a pMDP, and P is a probability distribution
over the parameter space V M . If M is a pMC, then we call M P a uMC.
Intuitively, a uMDP is a pMDP with an associated distribution over possible
(graph-preserving) parameter instantiations. That is, a realization of P yields a
concrete MDP M[u] with the respective instantiation u ∈ V M (and P(u) > 0).
Remark 1. In a uMDP, we distinguish controllable and uncontrollable parameters.
The uncontrollable parameters follow the probability distribution P. In contrast,
we can actively instantiate the controllable parameters. In the following, we
specifically allow cost parameters to be controllable.
Definition 3 (Satisfaction Probability). Let M P = (M, P) be a uMDP and
ϕ a specification. The (weighted) satisfaction probability of ϕ is
F (M P , ϕ) =
V M
I ϕ (u) d P(u)
5 The theory also applies to lower bounded properties.
291
instantiation u is well-defined for M if the resulting model M[u] is an MDP. We
assume that all parameter instantiations in V M yield well-defined MDPs. We call
u graph-preserving if for all s, s
∈ S and α ∈ Act it holds that P(s, α, s
) = 0 ⇒
P(s, α, s
)[u] ∈ (0, 1]. If P(s, α, s
) ∈ {p, 1 − p | p ∈ V } ∪ Q, then the parameter
space V M is given by the rectangle [0, 1]
|V | . We also consider a state-action cost
function c : S × Act → Q[V ]. We denote the set of cost parameters as W.
To define measures on MDPs, nondeterministic choices are resolved by a
so-called policy σ : S → Act with σ(s) ∈ ActS (s). The set of all policies over
M is Str
M . For the specifications that we consider in this paper, memoryless
deterministic policies are sufficient [48]. Applying a policy to an MDP yields an
induced Markov chain where all nondeterminism is resolved.
For an MC D, the reachability specification ϕ r = P ≤λ (♦T ) asserts that a set
T ⊆ S of target states is reached with probability at most λ ∈ [0, 1]
5 . If ϕ r holds
for D, we write D |= ϕ r . Model checking for the more general PCTL [4] or ωregular specifications is often reducible to checking reachability specifications [48].
For an MDP M, ϕ r holds if for all σ ∈ Str
M such that the induced MC D by the
policy σ reaches the set T with a probability of at most λ. For an expected cost
specification ϕ c = EC ≤κ (♦G), it holds that D |= ϕ c if and only if the expected
cost of reaching a set G ⊆ S is at most κ ∈ R. The expected cost of reaching G
is well-defined if and only if P(♦T ) = 1 for all policies in an MDP.
2.2 Uncertain MDPs
We now introduce the setting that we study in this paper. Specifically, we use
parameters to define the uncertainty in the transition probabilities and cost
functions of an MDP. Each random parameter follows an unknown probability
distribution from which we can sample the parameter values.
Definition 2 (uMDP). An uncertain Markov decision process M P (uMDP)
is a tuple M P = (M, P) where M is a pMDP, and P is a probability distribution
over the parameter space V M . If M is a pMC, then we call M P a uMC.
Intuitively, a uMDP is a pMDP with an associated distribution over possible
(graph-preserving) parameter instantiations. That is, a realization of P yields a
concrete MDP M[u] with the respective instantiation u ∈ V M (and P(u) > 0).
Remark 1. In a uMDP, we distinguish controllable and uncontrollable parameters.
The uncontrollable parameters follow the probability distribution P. In contrast,
we can actively instantiate the controllable parameters. In the following, we
specifically allow cost parameters to be controllable.
Definition 3 (Satisfaction Probability). Let M P = (M, P) be a uMDP and
ϕ a specification. The (weighted) satisfaction probability of ϕ is
F (M P , ϕ) =
V M
I ϕ (u) d P(u)
5 The theory also applies to lower bounded properties.