352
F. Delgrange et al.
For an MILP instance as above, each of the n rows of the inequation system
Ax ≤ b represent a constraint that is linear over the integral and m real-valued
variables given by x. We call the constraints feasible if there is a solution to the
inequation system. The task is to decide whether the constraints are feasible
and if so, find a solution that maximizes a linear optimization function c
T
x.
The optimization function can be omitted if we are only interested in feasibility.
MILP is NP-complete [35]. However, tools such as Gurobi [27] and SCIP [26]
implement practically efficient algorithms that can solve large instances.
For the rest of this section, let M = S, Act , P, s I , Q = ψ 1 , . . . , ψ with
ψ j = E ∼j (R j ♦G j ), and p ∈ (R ∞ )
be an instance for PSMA. We provide a
translation of the PSMA instance to an instance for MILP that has a feasible
solution iff p ∈ Ach
M
PS (Q). The MILP encoding considers integer variables to
encode a pure stationary strategy σ ∈ Σ
M
PS . The other variables and constraints
encode the expected reward for each objective on the induced MC M
σ .
3.3 Unichain MDP and Finite Rewards
Restriction 1 (Unichain MDP). MDP M has exactly one end component.
Restriction 2 (Reward Finiteness). E
Ms
σ (R j ♦G j ) < ∞ holds for each objective ψ j = E ∼j (R j ♦G j ), state s, and pure stationary strategy σ.
For simplicity, we first explain our encoding for unichain MDP with finite reward.
Sect. 3.5 lifts Restriction 1 and Sect. 3.6 lifts Restriction 2 with more details given
in [17, App. B]. Sect. 3.4 presents an alternative to the encoding of this section,
which is smaller but restricted to total reward objectives.
Fig. 2 shows the MILP encoding in case Restrictions 1 and 2 hold. We assume
∀ j : pj = ∞ for the point p since (i) E
M
σ (R j ♦G j ) ≤ ∞ holds trivially and
(ii) E
M
σ (R j ♦G j ) ≥ ∞ will never hold due to Restriction 2. For j ∈ {1, . . . , ,},
let S
j
0 = {s ∈ S | ∀ σ ∈ Σ
M : E
M
σ (R j ♦G j ) = 0} and S
j
? = {s ∈ S \ S
j
0 |
s can be reached from s I without visiting a state in S
j
0 }. These sets can be obtained a priori by analyzing the graph structure of M [4]. Moreover, we consider upper bounds U
j
s ∈ Q for the expected reward at state s ∈ S
j
? such that
U
j
s ≥ max σ∈Σ M E
Ms
σ (R j ♦G j ). We compute such upper bounds using singleobjective model checking techniques [4,5]. The MILP encoding applies the characterization of expected rewards for MCs as a linear equation system [4].
Lemma 3. For every σ ∈ Σ
M
PS , the following equation system has a unique
solution Φ : {x s | s ∈ S} → R
|S| satisfying Φ(x s ) = E
Ms
σ (R j ♦G j ):
∀ s ∈ S
j
0 : x s = 0
∀ s ∈ S
j
? : x s =
s ∈S
P(s, σ(s), s
) ·
x s + R(s, σ(s), s
)
Mixed Integer Linear Programming Problem (MILP)
Input: m, n ∈ N, A ∈ Q
n×(+m) , b ∈ Q
n , c ∈ Q
+m
Output:
x ∈ arg max x∈X c
T
x if X X = ∅
infeasible
if X = ∅
with X = {x ∈ Z
× R
m
| Ax ≤ b}
F. Delgrange et al.
For an MILP instance as above, each of the n rows of the inequation system
Ax ≤ b represent a constraint that is linear over the integral and m real-valued
variables given by x. We call the constraints feasible if there is a solution to the
inequation system. The task is to decide whether the constraints are feasible
and if so, find a solution that maximizes a linear optimization function c
T
x.
The optimization function can be omitted if we are only interested in feasibility.
MILP is NP-complete [35]. However, tools such as Gurobi [27] and SCIP [26]
implement practically efficient algorithms that can solve large instances.
For the rest of this section, let M = S, Act , P, s I , Q = ψ 1 , . . . , ψ with
ψ j = E ∼j (R j ♦G j ), and p ∈ (R ∞ )
be an instance for PSMA. We provide a
translation of the PSMA instance to an instance for MILP that has a feasible
solution iff p ∈ Ach
M
PS (Q). The MILP encoding considers integer variables to
encode a pure stationary strategy σ ∈ Σ
M
PS . The other variables and constraints
encode the expected reward for each objective on the induced MC M
σ .
3.3 Unichain MDP and Finite Rewards
Restriction 1 (Unichain MDP). MDP M has exactly one end component.
Restriction 2 (Reward Finiteness). E
Ms
σ (R j ♦G j ) < ∞ holds for each objective ψ j = E ∼j (R j ♦G j ), state s, and pure stationary strategy σ.
For simplicity, we first explain our encoding for unichain MDP with finite reward.
Sect. 3.5 lifts Restriction 1 and Sect. 3.6 lifts Restriction 2 with more details given
in [17, App. B]. Sect. 3.4 presents an alternative to the encoding of this section,
which is smaller but restricted to total reward objectives.
Fig. 2 shows the MILP encoding in case Restrictions 1 and 2 hold. We assume
∀ j : pj = ∞ for the point p since (i) E
M
σ (R j ♦G j ) ≤ ∞ holds trivially and
(ii) E
M
σ (R j ♦G j ) ≥ ∞ will never hold due to Restriction 2. For j ∈ {1, . . . , ,},
let S
j
0 = {s ∈ S | ∀ σ ∈ Σ
M : E
M
σ (R j ♦G j ) = 0} and S
j
? = {s ∈ S \ S
j
0 |
s can be reached from s I without visiting a state in S
j
0 }. These sets can be obtained a priori by analyzing the graph structure of M [4]. Moreover, we consider upper bounds U
j
s ∈ Q for the expected reward at state s ∈ S
j
? such that
U
j
s ≥ max σ∈Σ M E
Ms
σ (R j ♦G j ). We compute such upper bounds using singleobjective model checking techniques [4,5]. The MILP encoding applies the characterization of expected rewards for MCs as a linear equation system [4].
Lemma 3. For every σ ∈ Σ
M
PS , the following equation system has a unique
solution Φ : {x s | s ∈ S} → R
|S| satisfying Φ(x s ) = E
Ms
σ (R j ♦G j ):
∀ s ∈ S
j
0 : x s = 0
∀ s ∈ S
j
? : x s =
s ∈S
P(s, σ(s), s
) ·
x s + R(s, σ(s), s
)
Mixed Integer Linear Programming Problem (MILP)
Input: m, n ∈ N, A ∈ Q
n×(+m) , b ∈ Q
n , c ∈ Q
+m
Output:
x ∈ arg max x∈X c
T
x if X X = ∅
infeasible
if X = ∅
with X = {x ∈ Z
× R
m
| Ax ≤ b}