316
E. M. Hahn et al.
sequences of transitions of length that occur in the LSCC L. We call this information
a gold-brim accepting end-component claim of length , -GAEC claim for short.
The term “gold-brim” in the definition indicates that this is a powerful approach,
but not one that can be implemented efficiently. We will define weaker, efficiently implementable notions of accepting end-component claims (AEC claims) later.
The AEC simulation game is very similar to the simulation game of Section 3.1.
Both players produce an infinite run of their respective automata. If the spoiler makes
an AEC claim, e.g., an -GAEC claim, we say that her run complies with it if, starting
with the transition when the AEC claim is made, all states, transitions, or sequences of
transitions in the claim appear infinitely often, and all states, transitions, and sequences
of transitions the claim excludes do not appear. For an -GAEC claim, this means that
all of the sequences of transitions of length in the claim occur infinitely often, and no
other sequence of length occurs henceforth.
Thus, like a classic simulation game, an -GAEC simulation game is started by the
spoiler, who places her pebble on an initial state of B. Next, the duplicator puts his
pebble on an initial state of A. The two players then take turns, always starting with
the spoiler choosing an input letter and an according transition from B, followed by the
duplicator choosing a transition for the same letter in A.
Different from the classic simulation game, in an -GAEC simulation game, the
spoiler has an additional move that she can (and, in order to win, has to) perform once
in the game: In addition to choosing a letter and a transition, she can claim that she
has reached an accepting end-component, and provide a complete list of sequences of
automata transitions of length that can henceforth occur. This store is maintained, and
never updated. It has no further effect on the rules of the game: Both players produce
an infinite run of their respective automata. The duplicator has four ways to win:
1. if the spoiler never makes an AEC claim,
2. if the run of A he constructs is accepting,
3. if the run the spoiler constructs on B does not comply with the AEC claim, and
4. if the run that the spoiler produces is not accepting.
For -GAEC claims, (4) simply means that the set of transitions defined by the sequences does not satisfy the B¨ uchi, parity, or Rabin acceptance condition.
Theorem 5. [-GAEC Simulation] If A and B are language equivalent automata, B is
GFM, and there exists an such that A -GAEC simulates B, then A is GFM.
For the proof, we use an arbitrary (but fixed) MDP M, and an arbitrary (but fixed)
pure optimal positional strategy μ for M×B, resulting in the Markov chain (M×B) μ .
We assume w.l.o.g. that the accepting LSCCs in (M × B) μ are identified, e.g., by a bit.
Let τ be a winning strategy of the duplicator in an -GAEC simulation game. Abusing notation, we let τ ◦ μ denote the finite-memory strategy
6 obtained from μ and τ for
M × A, where τ is acting only on the automata part of (M × B), and where the spoiler
6 The strategy τ consists of one sub-strategy to be used before the AEC claim is made and one
sub-strategy for each possible -GAEC claim. The memory of τ ◦ μ tracks the position in
(M × B) μ. When an accepting LSCC is detected (via the marker bit) analysis of (M × B)μ
reveals the only possible -GAEC claim. This claim is used to select the right entry from τ .
E. M. Hahn et al.
sequences of transitions of length that occur in the LSCC L. We call this information
a gold-brim accepting end-component claim of length , -GAEC claim for short.
The term “gold-brim” in the definition indicates that this is a powerful approach,
but not one that can be implemented efficiently. We will define weaker, efficiently implementable notions of accepting end-component claims (AEC claims) later.
The AEC simulation game is very similar to the simulation game of Section 3.1.
Both players produce an infinite run of their respective automata. If the spoiler makes
an AEC claim, e.g., an -GAEC claim, we say that her run complies with it if, starting
with the transition when the AEC claim is made, all states, transitions, or sequences of
transitions in the claim appear infinitely often, and all states, transitions, and sequences
of transitions the claim excludes do not appear. For an -GAEC claim, this means that
all of the sequences of transitions of length in the claim occur infinitely often, and no
other sequence of length occurs henceforth.
Thus, like a classic simulation game, an -GAEC simulation game is started by the
spoiler, who places her pebble on an initial state of B. Next, the duplicator puts his
pebble on an initial state of A. The two players then take turns, always starting with
the spoiler choosing an input letter and an according transition from B, followed by the
duplicator choosing a transition for the same letter in A.
Different from the classic simulation game, in an -GAEC simulation game, the
spoiler has an additional move that she can (and, in order to win, has to) perform once
in the game: In addition to choosing a letter and a transition, she can claim that she
has reached an accepting end-component, and provide a complete list of sequences of
automata transitions of length that can henceforth occur. This store is maintained, and
never updated. It has no further effect on the rules of the game: Both players produce
an infinite run of their respective automata. The duplicator has four ways to win:
1. if the spoiler never makes an AEC claim,
2. if the run of A he constructs is accepting,
3. if the run the spoiler constructs on B does not comply with the AEC claim, and
4. if the run that the spoiler produces is not accepting.
For -GAEC claims, (4) simply means that the set of transitions defined by the sequences does not satisfy the B¨ uchi, parity, or Rabin acceptance condition.
Theorem 5. [-GAEC Simulation] If A and B are language equivalent automata, B is
GFM, and there exists an such that A -GAEC simulates B, then A is GFM.
For the proof, we use an arbitrary (but fixed) MDP M, and an arbitrary (but fixed)
pure optimal positional strategy μ for M×B, resulting in the Markov chain (M×B) μ .
We assume w.l.o.g. that the accepting LSCCs in (M × B) μ are identified, e.g., by a bit.
Let τ be a winning strategy of the duplicator in an -GAEC simulation game. Abusing notation, we let τ ◦ μ denote the finite-memory strategy
6 obtained from μ and τ for
M × A, where τ is acting only on the automata part of (M × B), and where the spoiler
6 The strategy τ consists of one sub-strategy to be used before the AEC claim is made and one
sub-strategy for each possible -GAEC claim. The memory of τ ◦ μ tracks the position in
(M × B) μ. When an accepting LSCC is detected (via the marker bit) analysis of (M × B)μ
reveals the only possible -GAEC claim. This claim is used to select the right entry from τ .