Good-for-MDPs Automata
315
4 Accepting End-Component Simulation
An end-component [5,2] of an MDP M is a sub-MDP M
of M such that its underlying
graph is strongly connected. A maximal end-component is maximal under set-inclusion.
Every state of an MDP belongs to at most one maximal end-component.
Theorem 4 (End-Component Properties. Theorem 3.1 and Theorem 4.2 of [5]).
Once an end-component C of an MDP is entered, there is a strategy that visits every
state-action combination in C infinitely often with probability 1 and stays in C forever.
For a product MDP, an accepting end-component (AEC) is an end-component that
contains some transition in Γ
× . There is a positional pure strategy for an AEC C that
surely stays in C and almost surely visits a transition in Γ
× infinitely often.
For a product MDP, there is a set of disjoint accepting end-components such that,
from every state, the maximal probability to reach the union of these accepting endcomponents is the same as the maximal probability to satisfy Γ
× . Moreover, this probability can be realized by combining a positional pure (reachability) strategy outside of
this union with the aforementioned positional pure strategies for the individual AECs.
Lemma 1 shows that the GFM property is preserved by simulation: For languageequivalent automata A and B, if A simulates B and B is GFM, then A is also GFM.
However, a GFM automaton may not simulate a language-equivalent GFM automaton.
(See Figure 3.) Therefore we introduce a coarser preorder, Accepting End-Component
(AEC) simulation, that exploits the finiteness of the MDP M. We rely on Theorem 4 to
focus on positional pure strategies for M × B. Under such strategies, M × B becomes
a Markov chain [2] such that almost all its runs have the following properties:
– They will eventually reach a leaf strongly connected component (LSCC) in the
Markov chain.
– If they have reached a LSCC L, then, for all ∈ N, all sequences of transitions of
length in L occur infinitely often, and no other sequence of length occurs.
With this in mind, we can intuitively ask the spoiler to pick a run through this Markov
chain, and to disclose information about this run. Specifically, we can ask her to signal
when she has reached an accepting LSCC
5 in the Markov chain, and to provide information about this LSCC, in particular information entailed by the full list of sequences
of transitions of some fixed length described above. Runs that can be identified to
either not reach an accepting LSCC, to visit transitions not in this list, or to visit only a
subset of sequences from this list, form a 0 set. In the simulation game we define below,
we make use of this observation to discard such runs.
A simulation game can only use the syntactic material of the automata—-neither
the MDP nor the strategy are available. The information the spoiler may provide cannot explicitly refer to them. What the spoiler may be asked to provide is information
on when she has entered an accepting LSCC, and, once she has signaled this, which
sequences of length l of automata transitions of B occur in the LSCC. The sequences
of automata transitions are simply the projections on the automata transitions from the
5 There is nothing to show when a non-accepting LSCC is reached—if B rejects, then A may
reject too—nor when no LSCC is reached, as this occurs with probability 0.
315
4 Accepting End-Component Simulation
An end-component [5,2] of an MDP M is a sub-MDP M
of M such that its underlying
graph is strongly connected. A maximal end-component is maximal under set-inclusion.
Every state of an MDP belongs to at most one maximal end-component.
Theorem 4 (End-Component Properties. Theorem 3.1 and Theorem 4.2 of [5]).
Once an end-component C of an MDP is entered, there is a strategy that visits every
state-action combination in C infinitely often with probability 1 and stays in C forever.
For a product MDP, an accepting end-component (AEC) is an end-component that
contains some transition in Γ
× . There is a positional pure strategy for an AEC C that
surely stays in C and almost surely visits a transition in Γ
× infinitely often.
For a product MDP, there is a set of disjoint accepting end-components such that,
from every state, the maximal probability to reach the union of these accepting endcomponents is the same as the maximal probability to satisfy Γ
× . Moreover, this probability can be realized by combining a positional pure (reachability) strategy outside of
this union with the aforementioned positional pure strategies for the individual AECs.
Lemma 1 shows that the GFM property is preserved by simulation: For languageequivalent automata A and B, if A simulates B and B is GFM, then A is also GFM.
However, a GFM automaton may not simulate a language-equivalent GFM automaton.
(See Figure 3.) Therefore we introduce a coarser preorder, Accepting End-Component
(AEC) simulation, that exploits the finiteness of the MDP M. We rely on Theorem 4 to
focus on positional pure strategies for M × B. Under such strategies, M × B becomes
a Markov chain [2] such that almost all its runs have the following properties:
– They will eventually reach a leaf strongly connected component (LSCC) in the
Markov chain.
– If they have reached a LSCC L, then, for all ∈ N, all sequences of transitions of
length in L occur infinitely often, and no other sequence of length occurs.
With this in mind, we can intuitively ask the spoiler to pick a run through this Markov
chain, and to disclose information about this run. Specifically, we can ask her to signal
when she has reached an accepting LSCC
5 in the Markov chain, and to provide information about this LSCC, in particular information entailed by the full list of sequences
of transitions of some fixed length described above. Runs that can be identified to
either not reach an accepting LSCC, to visit transitions not in this list, or to visit only a
subset of sequences from this list, form a 0 set. In the simulation game we define below,
we make use of this observation to discard such runs.
A simulation game can only use the syntactic material of the automata—-neither
the MDP nor the strategy are available. The information the spoiler may provide cannot explicitly refer to them. What the spoiler may be asked to provide is information
on when she has entered an accepting LSCC, and, once she has signaled this, which
sequences of length l of automata transitions of B occur in the LSCC. The sequences
of automata transitions are simply the projections on the automata transitions from the
5 There is nothing to show when a non-accepting LSCC is reached—if B rejects, then A may
reject too—nor when no LSCC is reached, as this occurs with probability 0.