Good-for-MDPs Automata
317
makes the move to the end-component when she is in some LSCC B of (M × B) μ and
gives the full list of sequences of transitions of length that occur in B.
Proof. As B is good for MDPs, we only have to show that the chance of winning in
(M × A) τ ◦μ is at least the chance of winning in (M × B) μ . The chance of winning
in (M × B) μ is the chance of reaching an accepting LSCC in (M × B) μ . It is also the
chance of reaching an accepting LSCC L ∈ (M × B) μ and, after reaching L, to see
exactly the sequences of transitions of length that occur in L, and to see all of them
infinitely often.
By construction, τ ◦ μ will translate those runs into accepting runs of (M × A) τ ◦μ ,
such that the chance of an accepting run of (M × A) τ ◦μ is at least the chance of an
accepting run of (M × B) μ . As μ is optimal, the chance of winning in M × A is at
least the chance of winning in M × B. As B is GFM, this is the chance of M producing
a run accepted by B (and thus A) when controlled optimally, which is an upper bound
on the chance of winning in M × A.
An -GAEC simulation, especially for large , results in very large state spaces,
because the spoiler has to list all sequences of transitions of B of length that will
appear infinitely often. No other sequence of length may then appear in the run
7 . This
can, of course, be prohibitively expensive.
As a compromise, one can use coarser-grained information at the cost of reducing
the duplicator’s ability of winning the game. E.g., the spoiler could be asked to only
reveal a transition that is repeated infinitely often, plus (when using more powerful
acceptance conditions than B¨ uchi), some acceptance information, say the dominating
priority in a parity game or a winning Rabin pair. This type of coarse-grained claim can
be refined slightly by allowing the duplicator to change at any time the transition that
is to appear infinitely often to the transition just used by the spoiler. Generally, we say
that an AEC simulation game is any simulation game, where
– the spoiler provides a list of states, transitions, or sequences of transitions that will
occur infinitely often and a list of states, transitions, or sequences of transitions that
will not occur in the future when making her AEC claim, and
– the duplicator may be able to update this list based on his observations,
– there exists some -GAEC simulation game such that a winning strategy of the
spoiler translates into a winning strategy of the spoiler in the AEC simulation game.
The requirement that a winning spoiler strategy translates into a winning spoiler strategy
in an -GAEC game entails that AEC simulation games can prove the GFM property.
Corollary 2. [AEC Simulation] If A and B are language equivalent automata, B is
good for MDPs, and A AEC-simulates B, then A is good for MDPs.
7 The AEC claim provides information about the accepting LSCC in the product under the chosen pure positional strategy. When the AEC claim requires the exclusion of states, transitions,
or sequences of transitions, then they are therefore surely excluded, whereas when it requires
inclusion of, and thus inclusion of infinitely many occurrances of, states, trasitions, or sequences of transitions, then they (only) occur almost surely infinitely often. Yet, runs that do
not contain them all infinitely often form a zero set, and can thus be ignored.
317
makes the move to the end-component when she is in some LSCC B of (M × B) μ and
gives the full list of sequences of transitions of length that occur in B.
Proof. As B is good for MDPs, we only have to show that the chance of winning in
(M × A) τ ◦μ is at least the chance of winning in (M × B) μ . The chance of winning
in (M × B) μ is the chance of reaching an accepting LSCC in (M × B) μ . It is also the
chance of reaching an accepting LSCC L ∈ (M × B) μ and, after reaching L, to see
exactly the sequences of transitions of length that occur in L, and to see all of them
infinitely often.
By construction, τ ◦ μ will translate those runs into accepting runs of (M × A) τ ◦μ ,
such that the chance of an accepting run of (M × A) τ ◦μ is at least the chance of an
accepting run of (M × B) μ . As μ is optimal, the chance of winning in M × A is at
least the chance of winning in M × B. As B is GFM, this is the chance of M producing
a run accepted by B (and thus A) when controlled optimally, which is an upper bound
on the chance of winning in M × A.
An -GAEC simulation, especially for large , results in very large state spaces,
because the spoiler has to list all sequences of transitions of B of length that will
appear infinitely often. No other sequence of length may then appear in the run
7 . This
can, of course, be prohibitively expensive.
As a compromise, one can use coarser-grained information at the cost of reducing
the duplicator’s ability of winning the game. E.g., the spoiler could be asked to only
reveal a transition that is repeated infinitely often, plus (when using more powerful
acceptance conditions than B¨ uchi), some acceptance information, say the dominating
priority in a parity game or a winning Rabin pair. This type of coarse-grained claim can
be refined slightly by allowing the duplicator to change at any time the transition that
is to appear infinitely often to the transition just used by the spoiler. Generally, we say
that an AEC simulation game is any simulation game, where
– the spoiler provides a list of states, transitions, or sequences of transitions that will
occur infinitely often and a list of states, transitions, or sequences of transitions that
will not occur in the future when making her AEC claim, and
– the duplicator may be able to update this list based on his observations,
– there exists some -GAEC simulation game such that a winning strategy of the
spoiler translates into a winning strategy of the spoiler in the AEC simulation game.
The requirement that a winning spoiler strategy translates into a winning spoiler strategy
in an -GAEC game entails that AEC simulation games can prove the GFM property.
Corollary 2. [AEC Simulation] If A and B are language equivalent automata, B is
good for MDPs, and A AEC-simulates B, then A is good for MDPs.
7 The AEC claim provides information about the accepting LSCC in the product under the chosen pure positional strategy. When the AEC claim requires the exclusion of states, transitions,
or sequences of transitions, then they are therefore surely excluded, whereas when it requires
inclusion of, and thus inclusion of infinitely many occurrances of, states, trasitions, or sequences of transitions, then they (only) occur almost surely infinitely often. Yet, runs that do
not contain them all infinitely often form a zero set, and can thus be ignored.