290
M. Cubuktepe et al.
the probability distribution of the uncertainty sets is assumed to be known. The
paper formulates the policy synthesis problem as an (undecidable [30]) partially
observable Markov decision process (POMDP) synthesis problem and use offthe-shelf point-based POMDP methods [10,6]. The work in [27,25] consider the
verification of MDPs with convex uncertainties. However, the uncertainty sets
for different states in an MDP are restricted to be independent, which does not
hold in our problem setting where we have parameter dependencies.
Uncertainties in MDPs have received quite some attention in the artificial
intelligence and planning literatures. Interval MDPs [27,7] use probability intervals
in the transition probabilities. Dynamic programming, robust value iteration and
robust policy iteration have been developed for MDPs with uncertain transition
probabilities whose parameters are statistically independent, also referred to as
rectangular, to find a policy ensuring the highest expected total reward at a given
confidence level [14,25]. The work in [28] relaxes this independence assumption a
bit and determines a policy that satisfies a given performance with a pre-defined
confidence provided an observation history of the MDP is given by using conic
programming. State-of-the art exact methods can handle models of up to a few
hundred of states [42]. Multi-model MDPs [44] treat distributions over probability
and cost parameters and aim at finding a single policy maximizing a weighted
value function. For deterministic policies this problem is NP-hard, and it is
PSPACE-hard for history-dependent policies.
2 Preliminaries
A probability distribution over a finite set X is a function μ : X → [0, 1] ⊆ R with
x∈X μ(x) = 1. The set of all distributions on X is denoted by Distr (X). Let
V = {x 1 , . . . , x n } be a finite set of parameters over R
n . The set of polynomials
over V is denoted by Q[V ]. We denote the cardinality of a set U by |U|.
2.1 Parametric Models
Definition 1 (pMDP). A parametric Markov decision process (pMDP) M is
a tuple M = (S, Act , s I , V, P) with a finite set S of states, a finite set Act of
actions, an initial state s I ∈ S, a finite set V of real-valued variables (parameters)
and a transition function P : S × Act × S → Q[V ].
For s ∈ S, ActS (s) = {α ∈ Act | ∃s
∈ S, P(s, α, s
) = 0} is the set of
enabled actions at s. Without loss of generality, we require ActS (s) = ∅ for s ∈ S.
If |ActS (s)| = 1 for all s ∈ S, M is a parametric discrete-time Markov chain
(pMC). We denote the transition function for pMCs by P(s, s
).
A pMDP M is a Markov decision process (MDP) if the transition function
yields well-defined probability distributions, i.e., P : S × Act × S → [0, 1] and
s ∈S P(s, α, s
) = 1 for all s ∈ S and α ∈ ActS (s). We denote the parameter
space of M by V M . Applying an instantiation u ∈ V M to a pMDP M yields
the instantiated MDP M[u] by replacing each f ∈ Q[V ] in M by f [u]. An
M. Cubuktepe et al.
the probability distribution of the uncertainty sets is assumed to be known. The
paper formulates the policy synthesis problem as an (undecidable [30]) partially
observable Markov decision process (POMDP) synthesis problem and use offthe-shelf point-based POMDP methods [10,6]. The work in [27,25] consider the
verification of MDPs with convex uncertainties. However, the uncertainty sets
for different states in an MDP are restricted to be independent, which does not
hold in our problem setting where we have parameter dependencies.
Uncertainties in MDPs have received quite some attention in the artificial
intelligence and planning literatures. Interval MDPs [27,7] use probability intervals
in the transition probabilities. Dynamic programming, robust value iteration and
robust policy iteration have been developed for MDPs with uncertain transition
probabilities whose parameters are statistically independent, also referred to as
rectangular, to find a policy ensuring the highest expected total reward at a given
confidence level [14,25]. The work in [28] relaxes this independence assumption a
bit and determines a policy that satisfies a given performance with a pre-defined
confidence provided an observation history of the MDP is given by using conic
programming. State-of-the art exact methods can handle models of up to a few
hundred of states [42]. Multi-model MDPs [44] treat distributions over probability
and cost parameters and aim at finding a single policy maximizing a weighted
value function. For deterministic policies this problem is NP-hard, and it is
PSPACE-hard for history-dependent policies.
2 Preliminaries
A probability distribution over a finite set X is a function μ : X → [0, 1] ⊆ R with
x∈X μ(x) = 1. The set of all distributions on X is denoted by Distr (X). Let
V = {x 1 , . . . , x n } be a finite set of parameters over R
n . The set of polynomials
over V is denoted by Q[V ]. We denote the cardinality of a set U by |U|.
2.1 Parametric Models
Definition 1 (pMDP). A parametric Markov decision process (pMDP) M is
a tuple M = (S, Act , s I , V, P) with a finite set S of states, a finite set Act of
actions, an initial state s I ∈ S, a finite set V of real-valued variables (parameters)
and a transition function P : S × Act × S → Q[V ].
For s ∈ S, ActS (s) = {α ∈ Act | ∃s
∈ S, P(s, α, s
) = 0} is the set of
enabled actions at s. Without loss of generality, we require ActS (s) = ∅ for s ∈ S.
If |ActS (s)| = 1 for all s ∈ S, M is a parametric discrete-time Markov chain
(pMC). We denote the transition function for pMCs by P(s, s
).
A pMDP M is a Markov decision process (MDP) if the transition function
yields well-defined probability distributions, i.e., P : S × Act × S → [0, 1] and
s ∈S P(s, α, s
) = 1 for all s ∈ S and α ∈ ActS (s). We denote the parameter
space of M by V M . Applying an instantiation u ∈ V M to a pMDP M yields
the instantiated MDP M[u] by replacing each f ∈ Q[V ] in M by f [u]. An