312
E. M. Hahn et al.
This is just an easy means to move back and forth between functions and relations,
and helps one to visualize the maximal number of successors. We next define the variations of subset and breakpoint constructions that are used to define the well-known
limit deterministic GFM automata—which we use in our proofs—and the slim GFM
automata we construct. Let 3
Q :=
(S, S
) | S
S ⊆ Q
and 3
Q
+ :=
(S, S
) | S
⊆
S ⊆ Q
. We define the subset notation for the transitions and accepting transitions as
δ S , γ S : 2
Q
× Σ → 2
Q with
δ S : (S, σ) →
q
∈ Q | ∃q ∈ S. (q, σ, q
) ∈ Δ
and
γ S : (S, σ) →
q
∈ Q | ∃q ∈ S. (q, σ, q
) ∈ Γ
.
We define the raw breakpoint transitions δ R : 3
Q
×Σ→3
Q
+ as
(S, S
), σ
→
δ S (S, σ),
δ S (S
, σ) ∪ γ S (S, σ)
. In this construction, we follow the set of reachable states (first
set) and the states that are reachable while passing at least one of the accepting transitions (second set). To turn this into a breakpoint automaton, we reset the second set to
the empty set when it equals the first; the transitions where we reset the second set are
exactly the accepting ones. The breakpoint automaton D =
Σ, 3
Q , (Q 0 , ∅), δ B , γ B
is
defined such that, when δ R :
(S, S
), σ
→ (R, R
), then there are three cases:
1. if R = ∅, then δ B
(S, S
)
is undefined (or, if a complete automaton is preferred,
maps to a rejecting sink),
2. else, if R = R
, then δ B :
(S, S
), σ
→ (R, R
) is a non-accepting transition,
3. otherwise δ B , γ B :
(S, S
), σ
→ (R
, ∅) is an accepting transition.
Finally, we define transitions Δ SB ⊆ 2
Q
× Σ × 3
Q that lead from a subset to a breakpoint construction, and γ 2,1 : 3
Q
× Σ → 3
Q that promote the second set of a breakpoint
construction to the first set as follows.
1. Δ SB =
S, σ, (S
, ∅)
| ∅ = S
⊆ δ S (S, σ)
are non-accepting transitions,
2. if δ S (S
, σ) = γ S (S, σ) = ∅, then γ 2,1
(S, S
), σ
is undefined, and
3. otherwise γ 2,1 :
(S, S
), σ
→
δ S (S
, σ)∪γ S (S, σ), ∅
is an accepting transition.
We can now define standard limit deterministic good for MDP automata.
Theorem 1. [11] A =
Σ, 2
Q
∪ 3
Q , Q 0 , ndet(δ S ) ∪ Δ SB ∪ ndet(δ B ), ndet(γ B )
recognizes the same language as B. It is limit deterministic and good for MDPs.
We now show how to construct a slim GFM B¨ uchi automaton.
Theorem 2 (Slim GFM B ¨
uchi Automaton). The automaton
S =
Σ, 3
Q , (Q 0 , ∅), ndet(δ B ) ∪ ndet(γ 2,1 ), ndet(γ B ) ∪ ndet(γ 2,1 )
simulates A. S is slim, language equivalent to B, and good for MDPs.
Proof. S is slim: its set of transitions is the union of two sets of deterministic transitions. We show that S simulates A by defining a strategy in the simulation game, which
ensures that, if the spoiler produces a run S 0 . . . S j−1 (S j , S
j )(S j+1 , S
j+1 ) . . . for A,
E. M. Hahn et al.
This is just an easy means to move back and forth between functions and relations,
and helps one to visualize the maximal number of successors. We next define the variations of subset and breakpoint constructions that are used to define the well-known
limit deterministic GFM automata—which we use in our proofs—and the slim GFM
automata we construct. Let 3
Q :=
(S, S
) | S
S ⊆ Q
and 3
Q
+ :=
(S, S
) | S
⊆
S ⊆ Q
. We define the subset notation for the transitions and accepting transitions as
δ S , γ S : 2
Q
× Σ → 2
Q with
δ S : (S, σ) →
q
∈ Q | ∃q ∈ S. (q, σ, q
) ∈ Δ
and
γ S : (S, σ) →
q
∈ Q | ∃q ∈ S. (q, σ, q
) ∈ Γ
.
We define the raw breakpoint transitions δ R : 3
Q
×Σ→3
Q
+ as
(S, S
), σ
→
δ S (S, σ),
δ S (S
, σ) ∪ γ S (S, σ)
. In this construction, we follow the set of reachable states (first
set) and the states that are reachable while passing at least one of the accepting transitions (second set). To turn this into a breakpoint automaton, we reset the second set to
the empty set when it equals the first; the transitions where we reset the second set are
exactly the accepting ones. The breakpoint automaton D =
Σ, 3
Q , (Q 0 , ∅), δ B , γ B
is
defined such that, when δ R :
(S, S
), σ
→ (R, R
), then there are three cases:
1. if R = ∅, then δ B
(S, S
)
is undefined (or, if a complete automaton is preferred,
maps to a rejecting sink),
2. else, if R = R
, then δ B :
(S, S
), σ
→ (R, R
) is a non-accepting transition,
3. otherwise δ B , γ B :
(S, S
), σ
→ (R
, ∅) is an accepting transition.
Finally, we define transitions Δ SB ⊆ 2
Q
× Σ × 3
Q that lead from a subset to a breakpoint construction, and γ 2,1 : 3
Q
× Σ → 3
Q that promote the second set of a breakpoint
construction to the first set as follows.
1. Δ SB =
S, σ, (S
, ∅)
| ∅ = S
⊆ δ S (S, σ)
are non-accepting transitions,
2. if δ S (S
, σ) = γ S (S, σ) = ∅, then γ 2,1
(S, S
), σ
is undefined, and
3. otherwise γ 2,1 :
(S, S
), σ
→
δ S (S
, σ)∪γ S (S, σ), ∅
is an accepting transition.
We can now define standard limit deterministic good for MDP automata.
Theorem 1. [11] A =
Σ, 2
Q
∪ 3
Q , Q 0 , ndet(δ S ) ∪ Δ SB ∪ ndet(δ B ), ndet(γ B )
recognizes the same language as B. It is limit deterministic and good for MDPs.
We now show how to construct a slim GFM B¨ uchi automaton.
Theorem 2 (Slim GFM B ¨
uchi Automaton). The automaton
S =
Σ, 3
Q , (Q 0 , ∅), ndet(δ B ) ∪ ndet(γ 2,1 ), ndet(γ B ) ∪ ndet(γ 2,1 )
simulates A. S is slim, language equivalent to B, and good for MDPs.
Proof. S is slim: its set of transitions is the union of two sets of deterministic transitions. We show that S simulates A by defining a strategy in the simulation game, which
ensures that, if the spoiler produces a run S 0 . . . S j−1 (S j , S
j )(S j+1 , S
j+1 ) . . . for A,