Good-for-MDPs Automata
309
an alphabet, and L : S × A × S → Σ is the labeling function of the set of transitions.
For a state s ∈ S, A(s) denotes the set of actions available in s. For states s, s
∈ S and
a ∈ A(s), we have that T (s, a)(s
) equals Pr (s
|s, a).
A run of M is an ω-word s 0 , a 1 , . . . ∈ S × (A × S)
ω such that Pr (s i+1 |s i , a i+1 ) >
0 for all i ≥ 0. A finite run is a finite such sequence. For a run r = s 0 , a 1 , s 1 , . . .
we define the corresponding labeled run as L(r) = L(s 0 , a 1 , s 1 ), L(s 1 , a 2 , s 2 ), . . . ∈
Σ
ω . We write Ω(M) (Paths(M)) for the set of runs (finite runs) of M and Ω s (M)
(Paths s (M)) for the set of runs (finite runs) of M starting from state s. When the MDP
is clear from the context we drop the argument M.
A strategy in M is a function μ : Paths → D(A) such that supp(μ(r)) ⊆
A(last(r)), where supp(d) is the support of d and last(r) is the last state of r. Let
Ω
M
μ (s) denote the subset of runs Ω
M (s) that correspond to strategy μ and initial state
s. Let Π M be the set of all strategies. We say that a strategy μ is pure if μ(r) is a point
distribution for all runs r ∈ Paths and we say that μ is positional if last(r) = last(r
)
implies μ(r) = μ(r
) for all runs r, r
∈ Paths. The behavior of an MDP M under a
strategy μ with starting state s is defined on a probability space (Ω
μ
s , F
μ
s , Pr
μ
s ) over the
set of infinite runs of μ from s.
3 Good-for-MDP (GFM) Automata
Given an MDP M and an automaton A = Σ, Q, q 0 , Δ, Γ , we want to compute an
optimal strategy satisfying the objective that the run of M is in the language of A. We
define the semantic satisfaction probability for A and a strategy μ from state s as:
PSem
M
A (s, μ)= Pr
μ
s {r∈Ω
μ
s : L(r)∈L A } and PSem
M
A (s)= sup
μ∈Π M
PSem
M
A (s, μ)
.
When using automata for the analysis of MDPs, we need a syntactic variant of the acceptance condition. Given an MDP M = (S, A, T, Σ, L) with initial state s 0 ∈ S and
automaton A = Σ, Q, q 0 , Δ, Γ , the product M×A=(S×Q, (s 0 , q 0 ), A×Q, T
× , Γ
× )
is an MDP [17] augmented with an initial state (s 0 , q 0 ) and accepting transitions Γ
× .
The (partial) function T
× : (S × Q) × (A × Q) − D(S × Q) is defined by
T
× ((s, q), (a, q
))((s
, q
)) =
T (s, a)(s
) if (q, L(s, a, s
), q
) ∈ Δ
undefined otherwise.
Finally, Γ
×
⊆ (S ×Q)×(A×Q)×(S ×Q) is defined by ((s, q), (a, q
), (s
, q
)) ∈ Γ
×
if, and only if, (q, L(s, a, s
), q
) ∈ Γ and T (s, a)(s
) > 0. A strategy μ on the MDP
defines a strategy μ
× on the product, and vice versa. We define the syntactic satisfaction
probabilities as
PSyn
M
A ((s, q), μ
× ) = Pr
μ
s {r ∈ Ω
μ
×
(s,q) (M × A) : inf(r) ∩ Γ
×
= ∅} , and
PSyn
M
A (s) =
sup
μ × ∈Π M×A
PSyn
M
A ((s, q 0 ), μ
× )
.
Note that PSyn
M
A (s) = PSem
M
A (s) holds for a deterministic A. In general, PSyn
M
A (s)
≤ PSem
M
A (s) holds, but equality is not guaranteed because the optimal resolution of
nondeterministic choices may require access to future events (see Figure 1).
309
an alphabet, and L : S × A × S → Σ is the labeling function of the set of transitions.
For a state s ∈ S, A(s) denotes the set of actions available in s. For states s, s
∈ S and
a ∈ A(s), we have that T (s, a)(s
) equals Pr (s
|s, a).
A run of M is an ω-word s 0 , a 1 , . . . ∈ S × (A × S)
ω such that Pr (s i+1 |s i , a i+1 ) >
0 for all i ≥ 0. A finite run is a finite such sequence. For a run r = s 0 , a 1 , s 1 , . . .
we define the corresponding labeled run as L(r) = L(s 0 , a 1 , s 1 ), L(s 1 , a 2 , s 2 ), . . . ∈
Σ
ω . We write Ω(M) (Paths(M)) for the set of runs (finite runs) of M and Ω s (M)
(Paths s (M)) for the set of runs (finite runs) of M starting from state s. When the MDP
is clear from the context we drop the argument M.
A strategy in M is a function μ : Paths → D(A) such that supp(μ(r)) ⊆
A(last(r)), where supp(d) is the support of d and last(r) is the last state of r. Let
Ω
M
μ (s) denote the subset of runs Ω
M (s) that correspond to strategy μ and initial state
s. Let Π M be the set of all strategies. We say that a strategy μ is pure if μ(r) is a point
distribution for all runs r ∈ Paths and we say that μ is positional if last(r) = last(r
)
implies μ(r) = μ(r
) for all runs r, r
∈ Paths. The behavior of an MDP M under a
strategy μ with starting state s is defined on a probability space (Ω
μ
s , F
μ
s , Pr
μ
s ) over the
set of infinite runs of μ from s.
3 Good-for-MDP (GFM) Automata
Given an MDP M and an automaton A = Σ, Q, q 0 , Δ, Γ , we want to compute an
optimal strategy satisfying the objective that the run of M is in the language of A. We
define the semantic satisfaction probability for A and a strategy μ from state s as:
PSem
M
A (s, μ)= Pr
μ
s {r∈Ω
μ
s : L(r)∈L A } and PSem
M
A (s)= sup
μ∈Π M
PSem
M
A (s, μ)
.
When using automata for the analysis of MDPs, we need a syntactic variant of the acceptance condition. Given an MDP M = (S, A, T, Σ, L) with initial state s 0 ∈ S and
automaton A = Σ, Q, q 0 , Δ, Γ , the product M×A=(S×Q, (s 0 , q 0 ), A×Q, T
× , Γ
× )
is an MDP [17] augmented with an initial state (s 0 , q 0 ) and accepting transitions Γ
× .
The (partial) function T
× : (S × Q) × (A × Q) − D(S × Q) is defined by
T
× ((s, q), (a, q
))((s
, q
)) =
T (s, a)(s
) if (q, L(s, a, s
), q
) ∈ Δ
undefined otherwise.
Finally, Γ
×
⊆ (S ×Q)×(A×Q)×(S ×Q) is defined by ((s, q), (a, q
), (s
, q
)) ∈ Γ
×
if, and only if, (q, L(s, a, s
), q
) ∈ Γ and T (s, a)(s
) > 0. A strategy μ on the MDP
defines a strategy μ
× on the product, and vice versa. We define the syntactic satisfaction
probabilities as
PSyn
M
A ((s, q), μ
× ) = Pr
μ
s {r ∈ Ω
μ
×
(s,q) (M × A) : inf(r) ∩ Γ
×
= ∅} , and
PSyn
M
A (s) =
sup
μ × ∈Π M×A
PSyn
M
A ((s, q 0 ), μ
× )
.
Note that PSyn
M
A (s) = PSem
M
A (s) holds for a deterministic A. In general, PSyn
M
A (s)
≤ PSem
M
A (s) holds, but equality is not guaranteed because the optimal resolution of
nondeterministic choices may require access to future events (see Figure 1).