354
F. Delgrange et al.
objectives. However, Line 7 yields Φ(x
j
s,α ) = −U
j
s if α is not selected. Thus, in
Line 8 we add U
j
s for each of the (|Act (s)| − 1) non-selected actions.
Line 9 and our observations above yield E
Ms
σ (R j ♦G j ) ≥ Φ(x
j
sI ) ≥ pj for
maximizing and E
Ms
σ (R j ♦G j ) ≤ −Φ(x
j
sI ) ≤ pj for minimizing objectives.
Therefore, p is achievable if a solution Φ exists. On the other hand, if p is
achievable by some σ ∈ Σ
M
PS , the solution Φ exists with Φ(a s,α ) = σ(s)(α),
Φ(x
j
s ) = Φ(x
j
s,α ) = ±E
Ms
σ (R j ♦G j ) if α = σ(s), and Φ(v) = 0 for other v ∈ Var .
Theorem 2. For unichain M and finite rewards, the constraints in Fig. 2 are
feasible iff p ∈ Ach
M
PS (Q).
Proposition 1. The MILP encoding above considers O(|S| · |Act | · ) variables.
3.4 Alternative Encoding for Total Rewards
We now consider PSMA instances where all objectives ψ j = E ∼j (R j ♦G j ) are
expected total reward objectives, i.e., G j = ∅. For such instances, we can employ
an encoding from [23] (restated in Lemma 4) for GMA. In fact, we can often
translate reachability reward objectives to total reward objectives, e.g., if the
set of goal states can not be left or if all objectives consider the same goal states.
Lemma 4 ([23]). For S 0 ⊆ S, let Φ : Var → R ≥0 be an assignment of variables
Var = {y s,α | s ∈ S \ S 0 , α ∈ Act (s)} and let σ Φ be a stationary strategy satisfying σ Φ (s)(α) = Φ(y s,α )/
β∈Act (s) Φ(y s,β ) for all s ∈ S \ S 0 and α ∈ Act (s) for
which the denominator is non-zero. Then, Φ is a solution to the equation system
∀ s ∈ S \ S 0 :
α∈Act (s)
y s,α = [s = s I ] +
s ,α ∈pre(s)
P(s
, α
, s) · y s ,α
1 =
ys,α∈Var
y s,α ·
s ∈S0
P(s, α, s
)
iff Pr
M
σ Φ (♦S 0 ) = 1 and ∀ y s,α ∈ Var : Φ(y s,α ) = E
M
σΦ (R s,α ♦S 0 ) with reward
structure R s,α given by R s,α (ˆ s, ˆ
α, s
) = [ˆ s = s and ˆ
α = α].
In [23], the lemma is applied to decide achievability of multiple total reward objectives under strategies that are stationary, but not necessarily pure. Intuitively,
E
M
σΦ (R s,α ♦S 0 ) coincides with the expected number of times action α is taken at
state s until S 0 is reached. Since this value can be infinite if Pr
M
σ Φ (♦S 0 ) < 1, a
solution Φ can only exist if it induces a strategy that almost surely reaches S 0 .
The encoding for unichain MDP with finite rewards and total reward objectives is shown in Fig. 3, where S 0 =
j S
j
0 and S ? = S \ S 0 . We consider the
constraints in conjunction with Lines 1 and 2 from Fig. 2. Let Φ be a solution
and let σ be the strategy encoded by such a solution, i.e., σ(s)(α) = Φ(a s,α ).
Lines 10 to 12 reflect the equations of Lemma 4. Since M is unichain and
we assume finite rewards, there is just one end component in which no reward
can be collected. Hence, S 0 is almost surely reached. Line 10 ensures that the
F. Delgrange et al.
objectives. However, Line 7 yields Φ(x
j
s,α ) = −U
j
s if α is not selected. Thus, in
Line 8 we add U
j
s for each of the (|Act (s)| − 1) non-selected actions.
Line 9 and our observations above yield E
Ms
σ (R j ♦G j ) ≥ Φ(x
j
sI ) ≥ pj for
maximizing and E
Ms
σ (R j ♦G j ) ≤ −Φ(x
j
sI ) ≤ pj for minimizing objectives.
Therefore, p is achievable if a solution Φ exists. On the other hand, if p is
achievable by some σ ∈ Σ
M
PS , the solution Φ exists with Φ(a s,α ) = σ(s)(α),
Φ(x
j
s ) = Φ(x
j
s,α ) = ±E
Ms
σ (R j ♦G j ) if α = σ(s), and Φ(v) = 0 for other v ∈ Var .
Theorem 2. For unichain M and finite rewards, the constraints in Fig. 2 are
feasible iff p ∈ Ach
M
PS (Q).
Proposition 1. The MILP encoding above considers O(|S| · |Act | · ) variables.
3.4 Alternative Encoding for Total Rewards
We now consider PSMA instances where all objectives ψ j = E ∼j (R j ♦G j ) are
expected total reward objectives, i.e., G j = ∅. For such instances, we can employ
an encoding from [23] (restated in Lemma 4) for GMA. In fact, we can often
translate reachability reward objectives to total reward objectives, e.g., if the
set of goal states can not be left or if all objectives consider the same goal states.
Lemma 4 ([23]). For S 0 ⊆ S, let Φ : Var → R ≥0 be an assignment of variables
Var = {y s,α | s ∈ S \ S 0 , α ∈ Act (s)} and let σ Φ be a stationary strategy satisfying σ Φ (s)(α) = Φ(y s,α )/
β∈Act (s) Φ(y s,β ) for all s ∈ S \ S 0 and α ∈ Act (s) for
which the denominator is non-zero. Then, Φ is a solution to the equation system
∀ s ∈ S \ S 0 :
α∈Act (s)
y s,α = [s = s I ] +
s ,α ∈pre(s)
P(s
, α
, s) · y s ,α
1 =
ys,α∈Var
y s,α ·
s ∈S0
P(s, α, s
)
iff Pr
M
σ Φ (♦S 0 ) = 1 and ∀ y s,α ∈ Var : Φ(y s,α ) = E
M
σΦ (R s,α ♦S 0 ) with reward
structure R s,α given by R s,α (ˆ s, ˆ
α, s
) = [ˆ s = s and ˆ
α = α].
In [23], the lemma is applied to decide achievability of multiple total reward objectives under strategies that are stationary, but not necessarily pure. Intuitively,
E
M
σΦ (R s,α ♦S 0 ) coincides with the expected number of times action α is taken at
state s until S 0 is reached. Since this value can be infinite if Pr
M
σ Φ (♦S 0 ) < 1, a
solution Φ can only exist if it induces a strategy that almost surely reaches S 0 .
The encoding for unichain MDP with finite rewards and total reward objectives is shown in Fig. 3, where S 0 =
j S
j
0 and S ? = S \ S 0 . We consider the
constraints in conjunction with Lines 1 and 2 from Fig. 2. Let Φ be a solution
and let σ be the strategy encoded by such a solution, i.e., σ(s)(α) = Φ(a s,α ).
Lines 10 to 12 reflect the equations of Lemma 4. Since M is unichain and
we assume finite rewards, there is just one end component in which no reward
can be collected. Hence, S 0 is almost surely reached. Line 10 ensures that the