Good-for-MDPs Automata
313
then the duplicator produces a run (T 0 , T
0 ) . . . (T j−1 , T
j−1 )(T j , T
j )(T j+1 , T
j−1 ) . . .
for S, such that (1) S i ⊆ T i holds for all i ∈ ω, and (2) if there are two accepting transitions
(S k−1 , S
k−1 ), σ k , (S k , S
k )
and
(S l−1 , S
l−1 ), σ l , (S l , S
l )
with k < l, there
is an k < m ≤ l, such that
(T m−1 , T
m−1 ), σ m (T m , T
m )
is accepting.
To obtain this, we describe a winning strategy for the duplicator while arguing inductively that it mainains (1). Note that (1) holds initially (T 0 = S 0 , induction basis).
Initial Phase: Every move of the spoiler—with some letter σ—that uses a transition
from δ S —the subset part of A—is followed by a move from δ B with the same letter
σ. When the duplicator follows this strategy the following holds: when, after a pair of
moves, the pebble of the spoiler is on state S ⊆ Q, then the pebble of the duplicator is
on some state (S, S
). In particular, (1) is preserved during this phase (induction step).
Transition Phase: The one spoiler move—with some letter σ—that uses a transition
from Δ SB —the transition to the breakpoint part of A—is followed by a move from δ B
with the same letter σ. When the duplicator follows this strategy, and when, after the
pair of moves, the pebble of the spoiler is on state (S, ∅), then the pebble of the duplicator is on some state (T, T
) with S ⊆ T . In particular, (1) is preserved (induction step).
Final Phase: When the spoiler moves from some state (S, S
)—with some letter σ—
that uses a transition from δ B —the breakpoint part of A—to ( ¯
S, ¯
S
), and when the
duplicator is in some state (T, T
), then the duplicator does the following. He calculates ( ¯
T , ∅) = γ 2,1
(T, T
), σ
and checks if ¯
S ⊆ ¯
T holds. If ¯
S ⊆ ¯
T holds, he plays
this transition from γ 2,1 (with the same letter σ). Otherwise, he plays the transition from
δ B (with the same letter σ). In either case (1) is preserved (induction step), which closes
the inductive argument for (1).
Note that no accepting transition of A is passed in the initial or tansition phase, so
the two accepting transitions from (2) must both fall into the final phase.
To show (2), we first observe that S
k = ∅, and thus S
k ⊆ T
k holds. Assuming for
contradition that all transitions of S for σ k+1 . . . σ l−1 are non-accepting, we obtain—
using (1)—by a straightforward inductive argument that S
i ⊆ T
i for all i with k≤i
Using that S l = δ S (S
l−1 , σ l ) ∪ γ S (S l−1 , σ l ) ⊆ δ S (T
l−1 , σ l ) ∪ γ S (T l−1 , σ l ) holds,
the spoiler uses an accepting transition from γ 2,1 in this step.
Using Lemma 1, it now suffices to show that the language of S is included in the language of B. To show this, we simply argue that an accepting run ρ = (Q 0 , Q
0 ), (Q 1 , Q
1 ),
(Q 2 , Q
2 ), (Q 3 , Q
3 ), . . . of S on an input word α = σ 0 , σ 1 , σ 2 , . . . can be interpreted
as a forest of finitely many finitely branching trees of overall infinite size, where all
infinite branches are accepting runs of B. K˝ onig’s Lemma then proves the existence of
an accepting run of B.
This forest is the usual one. The nodes are labeled by states of B, and the roots (level
0) are the initial states of B. Let I =
i ∈ N |
(Q i−1 , Q
i−1 ), σ i−1 , (Q i , Q
i )
∈ Γ :=
ndet(γ B )∪ndet(γ 2,1 )
be the set of positions after accepting transitions in ρ. We define
the predecessor function pred : N → I∪{0} with pred : i → max
j ∈ I∪{0} | j < i
.
We call a node with label q l on level l an end-point if one of the following applies:
(1) q l /
∈ Q l or (2) l ∈ I and for all j such that pred(l) ≤ j < l, where q j is the label of
the ancestor of this node on level j, we have (q j , σ j , q j+1 ) /
∈ Γ .
313
then the duplicator produces a run (T 0 , T
0 ) . . . (T j−1 , T
j−1 )(T j , T
j )(T j+1 , T
j−1 ) . . .
for S, such that (1) S i ⊆ T i holds for all i ∈ ω, and (2) if there are two accepting transitions
(S k−1 , S
k−1 ), σ k , (S k , S
k )
and
(S l−1 , S
l−1 ), σ l , (S l , S
l )
with k < l, there
is an k < m ≤ l, such that
(T m−1 , T
m−1 ), σ m (T m , T
m )
is accepting.
To obtain this, we describe a winning strategy for the duplicator while arguing inductively that it mainains (1). Note that (1) holds initially (T 0 = S 0 , induction basis).
Initial Phase: Every move of the spoiler—with some letter σ—that uses a transition
from δ S —the subset part of A—is followed by a move from δ B with the same letter
σ. When the duplicator follows this strategy the following holds: when, after a pair of
moves, the pebble of the spoiler is on state S ⊆ Q, then the pebble of the duplicator is
on some state (S, S
). In particular, (1) is preserved during this phase (induction step).
Transition Phase: The one spoiler move—with some letter σ—that uses a transition
from Δ SB —the transition to the breakpoint part of A—is followed by a move from δ B
with the same letter σ. When the duplicator follows this strategy, and when, after the
pair of moves, the pebble of the spoiler is on state (S, ∅), then the pebble of the duplicator is on some state (T, T
) with S ⊆ T . In particular, (1) is preserved (induction step).
Final Phase: When the spoiler moves from some state (S, S
)—with some letter σ—
that uses a transition from δ B —the breakpoint part of A—to ( ¯
S, ¯
S
), and when the
duplicator is in some state (T, T
), then the duplicator does the following. He calculates ( ¯
T , ∅) = γ 2,1
(T, T
), σ
and checks if ¯
S ⊆ ¯
T holds. If ¯
S ⊆ ¯
T holds, he plays
this transition from γ 2,1 (with the same letter σ). Otherwise, he plays the transition from
δ B (with the same letter σ). In either case (1) is preserved (induction step), which closes
the inductive argument for (1).
Note that no accepting transition of A is passed in the initial or tansition phase, so
the two accepting transitions from (2) must both fall into the final phase.
To show (2), we first observe that S
k = ∅, and thus S
k ⊆ T
k holds. Assuming for
contradition that all transitions of S for σ k+1 . . . σ l−1 are non-accepting, we obtain—
using (1)—by a straightforward inductive argument that S
i ⊆ T
i for all i with k≤i
Using that S l = δ S (S
l−1 , σ l ) ∪ γ S (S l−1 , σ l ) ⊆ δ S (T
l−1 , σ l ) ∪ γ S (T l−1 , σ l ) holds,
the spoiler uses an accepting transition from γ 2,1 in this step.
Using Lemma 1, it now suffices to show that the language of S is included in the language of B. To show this, we simply argue that an accepting run ρ = (Q 0 , Q
0 ), (Q 1 , Q
1 ),
(Q 2 , Q
2 ), (Q 3 , Q
3 ), . . . of S on an input word α = σ 0 , σ 1 , σ 2 , . . . can be interpreted
as a forest of finitely many finitely branching trees of overall infinite size, where all
infinite branches are accepting runs of B. K˝ onig’s Lemma then proves the existence of
an accepting run of B.
This forest is the usual one. The nodes are labeled by states of B, and the roots (level
0) are the initial states of B. Let I =
i ∈ N |
(Q i−1 , Q
i−1 ), σ i−1 , (Q i , Q
i )
∈ Γ :=
ndet(γ B )∪ndet(γ 2,1 )
be the set of positions after accepting transitions in ρ. We define
the predecessor function pred : N → I∪{0} with pred : i → max
j ∈ I∪{0} | j < i
.
We call a node with label q l on level l an end-point if one of the following applies:
(1) q l /
∈ Q l or (2) l ∈ I and for all j such that pred(l) ≤ j < l, where q j is the label of
the ancestor of this node on level j, we have (q j , σ j , q j+1 ) /
∈ Γ .