356
F. Delgrange et al.
∀ j ∈ {1, . . . , ,} , E ∈ MECS (ME
j
? ) :
Detect states with zero reward
∀ s ∈ SE :
±x
j
s ≤ U
j
s · (1 − e
j
s )
(15)
∀ ∀s, α ∈ E :
e
j
s,α ∈ {0, as,α}
(16)
∀ s
∈ succ(s, α) :
e
j
s,α ≤ e
j
s
(17)
∀ s ∈ SE :
e
j
s =
α∈Act (s)
[s, α ∈ E] · e
j
s,α
(18)
∀ α ∈ Act(s) :
z
j
s,α ∈ [0, Vs · as,α]
(19)
z
j
s,⊥ ∈ [0, Vs · e
j
s ]
(20)
z
j
s,⊥ +
α∈Act (s)
z
j
s,α =
1
|SE|
+
s ,α ∈pre(s)∩E
P(s
, α
, s) · z
j
s ,α
(21)
1 =
s∈SE
z
ψ j
s,⊥ +
α∈Act (s)
[s, α /
∈ E] · z
j
s,α
(22)
Figure 4: MILP encoding for detection of end components.
S
j
? -states. These ECs correspond to the ECs of the sub-MDP ME
j
? , where E
j
? is
the largest subset of S
j
? ×Act that is closed for M. For each E ∈ MECS (ME
j
? ),
we need to detect whether the encoded strategy induces a BSCC E
⊆ E.
To cope with multiple ECs, we consider the constraints from Fig. 2 in conjunction with the constraints from Fig. 4. Let Φ be a solution to these constraints
and let σ be the encoded strategy σ with σ(s)(α) = Φ(a s,α ). For each objective
ψ j and state s, a binary variable e
j
s is set to 1 if s lies on a BSCC of the induced
MC M
σ . We only need to consider states s ∈ SE for E ∈ MECS (ME
j
? ).
Line 15 ensures that the value of x
j
s is set to 0 if s lies on a BSCC of M
σ .
Lines 16 to 18 introduce binary variables e
j
s,α for each state-action pair in the EC
such that any solution Φ satisfies Φ(e
j
s,α ) = 1 iff Φ(e
j
s ) = Φ(a s,α ) = 1. Line 17
yields that Φ(e
j
s,α ) = 1 implies Φ(e
j
s ) = 1 for all successors s
of s and the
selected action α. Hence, for all s with Φ(e
j
s ) = 1 and for all s
reachable from s
in M
σ , we have Φ(e
j
s ) = 1 and s
, σ(s
) ∈ E. Therefore, we can only set e
j
s to 1
if there is a BSCC E
⊆ E that either contains s or that is almost surely reached
from s without leaving E. As finite rewards are assumed, E can not contain a
transition with positive reward, yielding E
M
σ (R j ♦G j ) = 0 if Φ(e
j
s ) = 1.
An assignment that sets all variables e
j
s and e
j
s,α to 0 trivially satisfies the
constraints in Lines 15 to 18. In Lines 19 to 22 we therefore ensure that if a BSCC
E
⊆ E exists in M
σ , Φ(e
j
s ) = 1 holds for at least one s ∈ SE
. The idea is based
on the observation that if a BSCC E
⊆ E exists, there is a state s ∈ SE that
does not reach the set S \ SE almost surely. We consider the MDP M
E , a mild
extension of ME given by M
E = (SE
s
E
I , s
E
⊥
, Act {α I , ⊥} , P
E , s
E
I ),
where P
E extends PE such that P
E (s
E
⊥ , ⊥, s
E
⊥ ) = 1 and ∀ s ∈ SE :
– P
E (s
E
I , α I , s) = 1/|SE|, P
E (s, ⊥, s
E
⊥ ) = 1, and
– ∀ α ∈ {ˆ α ∈ Act (s) | |s, ˆ
α /
∈ E} : P
E (s, α, s
E
⊥ ) = 1.
Lines 21 and 22 reflect the equation system from Lemma 4 for MDP M
E and
S 0 = {s ⊥ }. Additionally, Lines 19 and 20 exclude negative solutions and assert
F. Delgrange et al.
∀ j ∈ {1, . . . , ,} , E ∈ MECS (ME
j
? ) :
Detect states with zero reward
∀ s ∈ SE :
±x
j
s ≤ U
j
s · (1 − e
j
s )
(15)
∀ ∀s, α ∈ E :
e
j
s,α ∈ {0, as,α}
(16)
∀ s
∈ succ(s, α) :
e
j
s,α ≤ e
j
s
(17)
∀ s ∈ SE :
e
j
s =
α∈Act (s)
[s, α ∈ E] · e
j
s,α
(18)
∀ α ∈ Act(s) :
z
j
s,α ∈ [0, Vs · as,α]
(19)
z
j
s,⊥ ∈ [0, Vs · e
j
s ]
(20)
z
j
s,⊥ +
α∈Act (s)
z
j
s,α =
1
|SE|
+
s ,α ∈pre(s)∩E
P(s
, α
, s) · z
j
s ,α
(21)
1 =
s∈SE
z
ψ j
s,⊥ +
α∈Act (s)
[s, α /
∈ E] · z
j
s,α
(22)
Figure 4: MILP encoding for detection of end components.
S
j
? -states. These ECs correspond to the ECs of the sub-MDP ME
j
? , where E
j
? is
the largest subset of S
j
? ×Act that is closed for M. For each E ∈ MECS (ME
j
? ),
we need to detect whether the encoded strategy induces a BSCC E
⊆ E.
To cope with multiple ECs, we consider the constraints from Fig. 2 in conjunction with the constraints from Fig. 4. Let Φ be a solution to these constraints
and let σ be the encoded strategy σ with σ(s)(α) = Φ(a s,α ). For each objective
ψ j and state s, a binary variable e
j
s is set to 1 if s lies on a BSCC of the induced
MC M
σ . We only need to consider states s ∈ SE for E ∈ MECS (ME
j
? ).
Line 15 ensures that the value of x
j
s is set to 0 if s lies on a BSCC of M
σ .
Lines 16 to 18 introduce binary variables e
j
s,α for each state-action pair in the EC
such that any solution Φ satisfies Φ(e
j
s,α ) = 1 iff Φ(e
j
s ) = Φ(a s,α ) = 1. Line 17
yields that Φ(e
j
s,α ) = 1 implies Φ(e
j
s ) = 1 for all successors s
of s and the
selected action α. Hence, for all s with Φ(e
j
s ) = 1 and for all s
reachable from s
in M
σ , we have Φ(e
j
s ) = 1 and s
, σ(s
) ∈ E. Therefore, we can only set e
j
s to 1
if there is a BSCC E
⊆ E that either contains s or that is almost surely reached
from s without leaving E. As finite rewards are assumed, E can not contain a
transition with positive reward, yielding E
M
σ (R j ♦G j ) = 0 if Φ(e
j
s ) = 1.
An assignment that sets all variables e
j
s and e
j
s,α to 0 trivially satisfies the
constraints in Lines 15 to 18. In Lines 19 to 22 we therefore ensure that if a BSCC
E
⊆ E exists in M
σ , Φ(e
j
s ) = 1 holds for at least one s ∈ SE
. The idea is based
on the observation that if a BSCC E
⊆ E exists, there is a state s ∈ SE that
does not reach the set S \ SE almost surely. We consider the MDP M
E , a mild
extension of ME given by M
E = (SE
s
E
I , s
E
⊥
, Act {α I , ⊥} , P
E , s
E
I ),
where P
E extends PE such that P
E (s
E
⊥ , ⊥, s
E
⊥ ) = 1 and ∀ s ∈ SE :
– P
E (s
E
I , α I , s) = 1/|SE|, P
E (s, ⊥, s
E
⊥ ) = 1, and
– ∀ α ∈ {ˆ α ∈ Act (s) | |s, ˆ
α /
∈ E} : P
E (s, α, s
E
⊥ ) = 1.
Lines 21 and 22 reflect the equation system from Lemma 4 for MDP M
E and
S 0 = {s ⊥ }. Additionally, Lines 19 and 20 exclude negative solutions and assert