310
E. M. Hahn et al.
a, b
b
a, b
a
1
2
: a
1
2
: b
Fig. 1. An NBA, which accepts all words over the alphabet {a, b}, that is not good for MDPs.
The dotted transitions are accepting. For the Markov chain on the right where the probability of
a and b is
1
2
, the chance that the automaton makes infinitely many correct predictions is 0
Definition 1 (GFM automata). An automaton A is good for MDPs if, for all MDPs
M, PSyn
M
A (s 0 ) = PSem
M
A (s 0 ) holds, where s 0 is the initial state of M.
For an automaton to match PSem
M
A (s 0 ), its nondeterminism is restricted not to rely
heavily on the future; rather, it must possible to resolve the nondeterminism on-the-fly.
For example, the B¨ uchi automaton presented on the left of Figure 1, which has to guess
whether the next symbol is a or b, is not good for MDPs, because the simple Markov
chain on the right of Figure 1 does not allow resolution of its nondeterminism on-the-fly.
There are three families of automata that are known to be good for MDPs: (1) deterministic automata, (2) good for games automata [15,18], and (3) limit deterministic
automata that satisfy a few side constraints [4,11,29].
A limit-deterministic B¨ uchi automaton (LDBA) is a nondeterministic B¨ uchi automaton (NBA) A = Σ, Q i ∪ Q f , q 0 , Δ, Γ such that Q i ∩ Q f = ∅; q 0 ∈ Q i ;
Γ ⊆ Q f × Σ × Q f ; (q, σ, q
), (q, σ, q
) ∈ Δ and q, q
∈ Q f implies q
= q
; and
(q, σ, q
) ∈ Δ and q ∈ Q f implies q
∈ Q f . An LDBA behaves deterministically once
it has seen an accepting transition. Usual LDBA constructions [11,29] produce GFM
automata. We refer to LDBAs with this property as suitable (SLDBAs), cf. Theorem 1.
In the context of RL, techniques based on SLDBAs are particularly useful, because
these automata use the B¨ uchi acceptance condition, which can be translated to reachability goals. Good for games and deterministic automata require more complex acceptance conditions, like parity, that do not have a natural translation into rewards [12].
Using SLDBA [4,11,29] has the drawback that they naturally have a high branching
degree in the initial part, as they naturally allow for many different transitions to the
accepting part of the LDBA. This can be avoided, but to the cost of a blow-up and a
more complex construction and data structure [29]. We therefore propose an automata
construction that produces NBAs with a small branching degree—it never produces
more than two successors. We call these automata slim. The resulting automata are not
(normally) limit deterministic, but we show that they are good for MDPs.
Due to technical dependencies we start with presenting a second observation, namely
that automata that simulate language equivalent GFM automata are GFM. As a side result, we observe that the same holds for good-for-games automata. The side result is not
surprising, as good-for-games automata were defined through simulation of deterministic automata [15]. But, to the best of our knowledge, the observation from Corollary
1 has not been made yet for good-for-games automata.
E. M. Hahn et al.
a, b
b
a, b
a
1
2
: a
1
2
: b
Fig. 1. An NBA, which accepts all words over the alphabet {a, b}, that is not good for MDPs.
The dotted transitions are accepting. For the Markov chain on the right where the probability of
a and b is
1
2
, the chance that the automaton makes infinitely many correct predictions is 0
Definition 1 (GFM automata). An automaton A is good for MDPs if, for all MDPs
M, PSyn
M
A (s 0 ) = PSem
M
A (s 0 ) holds, where s 0 is the initial state of M.
For an automaton to match PSem
M
A (s 0 ), its nondeterminism is restricted not to rely
heavily on the future; rather, it must possible to resolve the nondeterminism on-the-fly.
For example, the B¨ uchi automaton presented on the left of Figure 1, which has to guess
whether the next symbol is a or b, is not good for MDPs, because the simple Markov
chain on the right of Figure 1 does not allow resolution of its nondeterminism on-the-fly.
There are three families of automata that are known to be good for MDPs: (1) deterministic automata, (2) good for games automata [15,18], and (3) limit deterministic
automata that satisfy a few side constraints [4,11,29].
A limit-deterministic B¨ uchi automaton (LDBA) is a nondeterministic B¨ uchi automaton (NBA) A = Σ, Q i ∪ Q f , q 0 , Δ, Γ such that Q i ∩ Q f = ∅; q 0 ∈ Q i ;
Γ ⊆ Q f × Σ × Q f ; (q, σ, q
), (q, σ, q
) ∈ Δ and q, q
∈ Q f implies q
= q
; and
(q, σ, q
) ∈ Δ and q ∈ Q f implies q
∈ Q f . An LDBA behaves deterministically once
it has seen an accepting transition. Usual LDBA constructions [11,29] produce GFM
automata. We refer to LDBAs with this property as suitable (SLDBAs), cf. Theorem 1.
In the context of RL, techniques based on SLDBAs are particularly useful, because
these automata use the B¨ uchi acceptance condition, which can be translated to reachability goals. Good for games and deterministic automata require more complex acceptance conditions, like parity, that do not have a natural translation into rewards [12].
Using SLDBA [4,11,29] has the drawback that they naturally have a high branching
degree in the initial part, as they naturally allow for many different transitions to the
accepting part of the LDBA. This can be avoided, but to the cost of a blow-up and a
more complex construction and data structure [29]. We therefore propose an automata
construction that produces NBAs with a small branching degree—it never produces
more than two successors. We call these automata slim. The resulting automata are not
(normally) limit deterministic, but we show that they are good for MDPs.
Due to technical dependencies we start with presenting a second observation, namely
that automata that simulate language equivalent GFM automata are GFM. As a side result, we observe that the same holds for good-for-games automata. The side result is not
surprising, as good-for-games automata were defined through simulation of deterministic automata [15]. But, to the best of our knowledge, the observation from Corollary
1 has not been made yet for good-for-games automata.