Good-for-MDPs Automata
311
3.1 Simulating GFM
An automaton A simulates an automaton B if the duplicator wins the simulation game.
The simulation game is played between a duplicator and a spoiler, who each control a
pebble, which they move along the edges of A and B, respectively. The 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 a transition for that letter in B, followed
by the duplicator choosing a transition for the same letter in A. This way, both players
produce an infinite run of their respective automaton. The duplicator has two ways to
win a play of the game: if the run of A he constructs is accepting, and if the run the
spoiler constructs on B is rejecting. The duplicator wins this game if he has a winning
strategy, i.e., a recipe to move his pebble that guarantees that he wins. Such a winning
strategy is “good-for-games,” as it can only rely on the past. It can be used to transform
winning strategies of B, so that, if they were witnessing a good for games property or
were good for an MDP, then the resulting strategy for A has the same property.
Lemma 1 (Simulation Properties). For ω-automata A and B the following holds.
1. If A simulates B then L(A) ⊇ L(B).
2. If A simulates B and L(A) ⊆ L(B) then L(A) = L(B).
3. If A simulates B, L(A) = L(B), and B is GFG, then A is GFG.
4. If A simulates B, L(A) = L(B), and B is GFM, then A is GFM.
Proof. Facts (1) and (2) are well known observations. Fact (1) holds because an accepting run of B on a word α can be translated into an accepting run of A on α by using the
winning strategy of A in the simulation game. Fact (2) follows immediately from Fact
(1). Facts (3) and (4) follow by simulating the behaviour of B on each run.
This observation allows us to use a family of state-space reduction techniques, in particular those based on language preserving translations for B¨ uchi automata based on
simulation relation [7,31,10,9]. This requires stronger notions of simulations, like direct and delayed simulation [9]. For the deterministic part of an LDBA, one can also
use space reduction techniques for DBAs like [25].
Corollary 1. All statespace reduction techniques that turn an NBA A into an NBA B
that simulates A preserve GFG and GFM: if A is GFG or GFM, then B is GFG or
GFM, respectively.
3.2 Constructing Slim GFM Automata
Let us fix B¨ uchi automaton B =
Σ, Q, Q 0 , Δ, Γ
. We can write Δ as a function
ˆ
δ : Q × Σ → 2
Q with ˆ
δ : (q, σ) → {q
∈ Q | (q, σ, q
) ∈ Δ}, which can be lifted
to sets, using the deterministic transition function δ : 2
Q
× Σ → 2
Q with δ : (S, σ) →
q∈S
ˆ
δ(q, σ). We also define an operator, ndet, that translates deterministic transition
functions δ : R × Σ → R to relations, using
ndet : (R × Σ → R) → 2
R×Σ×R
with ndet : δ →
(q, σ, q
) | q
∈ δ({q}, σ)
.
311
3.1 Simulating GFM
An automaton A simulates an automaton B if the duplicator wins the simulation game.
The simulation game is played between a duplicator and a spoiler, who each control a
pebble, which they move along the edges of A and B, respectively. The 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 a transition for that letter in B, followed
by the duplicator choosing a transition for the same letter in A. This way, both players
produce an infinite run of their respective automaton. The duplicator has two ways to
win a play of the game: if the run of A he constructs is accepting, and if the run the
spoiler constructs on B is rejecting. The duplicator wins this game if he has a winning
strategy, i.e., a recipe to move his pebble that guarantees that he wins. Such a winning
strategy is “good-for-games,” as it can only rely on the past. It can be used to transform
winning strategies of B, so that, if they were witnessing a good for games property or
were good for an MDP, then the resulting strategy for A has the same property.
Lemma 1 (Simulation Properties). For ω-automata A and B the following holds.
1. If A simulates B then L(A) ⊇ L(B).
2. If A simulates B and L(A) ⊆ L(B) then L(A) = L(B).
3. If A simulates B, L(A) = L(B), and B is GFG, then A is GFG.
4. If A simulates B, L(A) = L(B), and B is GFM, then A is GFM.
Proof. Facts (1) and (2) are well known observations. Fact (1) holds because an accepting run of B on a word α can be translated into an accepting run of A on α by using the
winning strategy of A in the simulation game. Fact (2) follows immediately from Fact
(1). Facts (3) and (4) follow by simulating the behaviour of B on each run.
This observation allows us to use a family of state-space reduction techniques, in particular those based on language preserving translations for B¨ uchi automata based on
simulation relation [7,31,10,9]. This requires stronger notions of simulations, like direct and delayed simulation [9]. For the deterministic part of an LDBA, one can also
use space reduction techniques for DBAs like [25].
Corollary 1. All statespace reduction techniques that turn an NBA A into an NBA B
that simulates A preserve GFG and GFM: if A is GFG or GFM, then B is GFG or
GFM, respectively.
3.2 Constructing Slim GFM Automata
Let us fix B¨ uchi automaton B =
Σ, Q, Q 0 , Δ, Γ
. We can write Δ as a function
ˆ
δ : Q × Σ → 2
Q with ˆ
δ : (q, σ) → {q
∈ Q | (q, σ, q
) ∈ Δ}, which can be lifted
to sets, using the deterministic transition function δ : 2
Q
× Σ → 2
Q with δ : (S, σ) →
q∈S
ˆ
δ(q, σ). We also define an operator, ndet, that translates deterministic transition
functions δ : R × Σ → R to relations, using
ndet : (R × Σ → R) → 2
R×Σ×R
with ndet : δ →
(q, σ, q
) | q
∈ δ({q}, σ)
.