318
E. M. Hahn et al.
a0
a1
a2
A
a, b, c
a, b, c
a, b, c
a, b, c
a
a, b, c
b
b0
B
b1
a, b
c
a, b, c
Fig. 3. Automata A (left) and B (right) for ϕ = (G F a) ∨ (G F b). The dotted transitions are
accepting. The NBA A does not simulate the DBA B: B can play a’s until A moves to either
the state on the left, or the state on the right. B then wins by henceforth playing only b’s or only
a’s. However, A is good for MDPs. It wins the AEC simulation game by waiting until an AEC
is reached (by B), and then check if a or b occurs infinitely often in this AEC. Based on this
knowledge, A can make its decision. This can be shown by AEC simulation if B has to provide
sufficient information, such as a list of transitions—or even a list of letters—that occur infinitely
often. The amount of information the spoiler has to provide determines the strength of the AEC
simulation used. If, e.g., B only has to reveal one accepting transition of the end-component,
then it can select an end-component where the revealed transition is (b 1, c, b0), which does not
provide sufficient information. Whereas, if the duplicator is allowed to update the transition, then
the duplicator wins by updating the recorded transition to the next a or b transition
Of course, for every AEC simulation, one first has to prove that winning strategies for
the spoiler translate. We have used two simple variations of the AEC simulation games:
accepting transition: the spoiler may only make her AEC claim when taking an accepting transition; this transition—and no other information—is stored, and the spoiler
commits to—and commits only to—seeing this transition infinitely often;
accepting transition with update: different to the accepting transition AEC simulation
game, the duplicator can—but does not have to—update the stored accepting transition
whenever the spoiler passes by an accepting transition.
Theorem 6. Both, the accepted transition and the accepted transition with update AEC
simulation, can be used to establish the good for MDPs property.
To show this, we describe the strategy translations in accordance with Corollary 2.
Proof. In both cases, the translation of a winning strategy of the spoiler for the 1-GAEC
simulation game are straightforward: The spoiler essentially follows her winning strategy from the 1-GAEC simulation game, with the extra rule that she will make her AEC
claim to the duplicator on the first accepting transition on or after her AEC claim in the
1-GAEC claim. If the duplicator is allowed to update the transition, this information is
ignored by the spoiler—she plays according to her winning strategy from the 1-GAEC
simulation game. Naturally, the resulting play will comply with her 1-GAEC claim, and
will thus also be winning for the—weaker—AEC claim made to the duplicator.
We use AEC simulation to identify GFM automata among the automata produced
(e.g., by SPOT [8]) at the beginning of the transformation. Figure 3 shows an example
for which the duplicator wins the AEC simulation game, but loses the ordinary simulation game. Candidates for automata to simulate are, e.g., the slim GFM B¨ uchi automata
and the limit deterministic B¨ uchi automata discussed above.
E. M. Hahn et al.
a0
a1
a2
A
a, b, c
a, b, c
a, b, c
a, b, c
a
a, b, c
b
b0
B
b1
a, b
c
a, b, c
Fig. 3. Automata A (left) and B (right) for ϕ = (G F a) ∨ (G F b). The dotted transitions are
accepting. The NBA A does not simulate the DBA B: B can play a’s until A moves to either
the state on the left, or the state on the right. B then wins by henceforth playing only b’s or only
a’s. However, A is good for MDPs. It wins the AEC simulation game by waiting until an AEC
is reached (by B), and then check if a or b occurs infinitely often in this AEC. Based on this
knowledge, A can make its decision. This can be shown by AEC simulation if B has to provide
sufficient information, such as a list of transitions—or even a list of letters—that occur infinitely
often. The amount of information the spoiler has to provide determines the strength of the AEC
simulation used. If, e.g., B only has to reveal one accepting transition of the end-component,
then it can select an end-component where the revealed transition is (b 1, c, b0), which does not
provide sufficient information. Whereas, if the duplicator is allowed to update the transition, then
the duplicator wins by updating the recorded transition to the next a or b transition
Of course, for every AEC simulation, one first has to prove that winning strategies for
the spoiler translate. We have used two simple variations of the AEC simulation games:
accepting transition: the spoiler may only make her AEC claim when taking an accepting transition; this transition—and no other information—is stored, and the spoiler
commits to—and commits only to—seeing this transition infinitely often;
accepting transition with update: different to the accepting transition AEC simulation
game, the duplicator can—but does not have to—update the stored accepting transition
whenever the spoiler passes by an accepting transition.
Theorem 6. Both, the accepted transition and the accepted transition with update AEC
simulation, can be used to establish the good for MDPs property.
To show this, we describe the strategy translations in accordance with Corollary 2.
Proof. In both cases, the translation of a winning strategy of the spoiler for the 1-GAEC
simulation game are straightforward: The spoiler essentially follows her winning strategy from the 1-GAEC simulation game, with the extra rule that she will make her AEC
claim to the duplicator on the first accepting transition on or after her AEC claim in the
1-GAEC claim. If the duplicator is allowed to update the transition, this information is
ignored by the spoiler—she plays according to her winning strategy from the 1-GAEC
simulation game. Naturally, the resulting play will comply with her 1-GAEC claim, and
will thus also be winning for the—weaker—AEC claim made to the duplicator.
We use AEC simulation to identify GFM automata among the automata produced
(e.g., by SPOT [8]) at the beginning of the transformation. Figure 3 shows an example
for which the duplicator wins the AEC simulation game, but loses the ordinary simulation game. Candidates for automata to simulate are, e.g., the slim GFM B¨ uchi automata
and the limit deterministic B¨ uchi automata discussed above.