308
E. M. Hahn et al.
able subset of the reachable states when progressing to the deterministic part of the
automaton, meaning a number of choices that is exponential in the NBA. We show that
we can instead use slim automata in Section 3.2 as a first example of NBAs that are
good-for-MDPs, but not limit deterministic. They have the appealing property that their
branching degree is at most two, while keeping the B¨ uchi acceptance mechanism that
works well with RL [12]. (Slim automata can also be used for model checking, but they
don’t provide similar advantages over suitable LDBAs there, because the backwards
analysis used in model checking makes selecting the correct successor trivial.)
Cautiousness and forgiveness are further properties, which are—while harder to
quantify—very desirable for RL: LDBAs, for example, suffer from having to make
a correct choice when moving into the deterministic part of the automaton, and they
have to make this correct choice from a very large set of nondeterministic transitions.
While this is unproblematic for standard model checking algorithms that are based on
backwards analysis, applications like RL that rely on forward analysis can be badly
affected when more (wrong) choices are offered, and when wrong choices cannot be
rectified. Cautiousness and forgiveness are a references to this: an automaton is more
cautious if it has less scope for making wrong decisions and more forgiving if it allows
for correcting previously made decisions (cf. Figure 5 for an example). Our experiments
(cf. Section 5) indicate that cautiousness and forgiveness are beneficial for RL.
Organization of the Paper. After the preliminaries, we introduce the “good-for-MDP”
property (Section 3) and show that it is preserved by simulation, which enables all
minimization techniques that offer the simulation property (Section 3.1). In Section 3.2
we use this observation to construct slim automata—NBAs with a branching degree of
2 that are neither limit deterministic nor good-for-games—as an example of a class of
automata that becomes available for MDP model checking and RL. We then introduce
a more powerful simulation relation, AEC simulation, that suffices to establish that an
automaton is good-for-MDPs (Section 4). In Section 5, we evaluate the impact of the
contributions of the paper on model checking and reinforcement learning algorithms.
2 Preliminaries
A nondeterministic B¨ uchi automaton is a tuple A = Σ, Q, q 0 , Δ, Γ , where Σ is a
finite alphabet, Q is a finite set of states, q 0 ∈ Q is the initial state, Δ ⊆ Q × Σ × Q
are transitions, and Γ ⊆ Q × Σ × Q is the transition-based acceptance condition.
A run r of A on w ∈ Σ
ω is an ω-word r 0 , w 0 , r 1 , w 1 , . . . in (Q×Σ)
ω such that r 0 =
q 0 and, for i > 0, it is (r i−1 , w i−1 , r i ) ∈ Δ. We write inf(r) for the set of transitions
that appear infinitely often in the run r. A run r of A is accepting if inf(r) ∩ Γ = ∅.
The language, L A , of A (or, recognized by A) is the subset of words in Σ
ω that have
accepting runs in A. A language is ω-regular if it is accepted by a B¨ uchi automaton. An
automaton A = Σ, Q, Q 0 , Δ, Γ is deterministic if (q, σ, q
), (q, σ, q
) ∈ Δ implies
q
= q
. A is complete if, for all σ ∈ Σ and all q ∈ Q, there is a transition (q, σ, q
) ∈
Δ. A word in Σ
ω has exactly one run in a deterministic, complete automaton.
A Markov decision process (MDP) M is a tuple (S, A, T, Σ, L) where S is a finite
set of states, A is a finite set of actions, T : S × A − D(S), where D(S) is the set of
probability distributions over S, is the probabilistic transition (partial) function, Σ is
E. M. Hahn et al.
able subset of the reachable states when progressing to the deterministic part of the
automaton, meaning a number of choices that is exponential in the NBA. We show that
we can instead use slim automata in Section 3.2 as a first example of NBAs that are
good-for-MDPs, but not limit deterministic. They have the appealing property that their
branching degree is at most two, while keeping the B¨ uchi acceptance mechanism that
works well with RL [12]. (Slim automata can also be used for model checking, but they
don’t provide similar advantages over suitable LDBAs there, because the backwards
analysis used in model checking makes selecting the correct successor trivial.)
Cautiousness and forgiveness are further properties, which are—while harder to
quantify—very desirable for RL: LDBAs, for example, suffer from having to make
a correct choice when moving into the deterministic part of the automaton, and they
have to make this correct choice from a very large set of nondeterministic transitions.
While this is unproblematic for standard model checking algorithms that are based on
backwards analysis, applications like RL that rely on forward analysis can be badly
affected when more (wrong) choices are offered, and when wrong choices cannot be
rectified. Cautiousness and forgiveness are a references to this: an automaton is more
cautious if it has less scope for making wrong decisions and more forgiving if it allows
for correcting previously made decisions (cf. Figure 5 for an example). Our experiments
(cf. Section 5) indicate that cautiousness and forgiveness are beneficial for RL.
Organization of the Paper. After the preliminaries, we introduce the “good-for-MDP”
property (Section 3) and show that it is preserved by simulation, which enables all
minimization techniques that offer the simulation property (Section 3.1). In Section 3.2
we use this observation to construct slim automata—NBAs with a branching degree of
2 that are neither limit deterministic nor good-for-games—as an example of a class of
automata that becomes available for MDP model checking and RL. We then introduce
a more powerful simulation relation, AEC simulation, that suffices to establish that an
automaton is good-for-MDPs (Section 4). In Section 5, we evaluate the impact of the
contributions of the paper on model checking and reinforcement learning algorithms.
2 Preliminaries
A nondeterministic B¨ uchi automaton is a tuple A = Σ, Q, q 0 , Δ, Γ , where Σ is a
finite alphabet, Q is a finite set of states, q 0 ∈ Q is the initial state, Δ ⊆ Q × Σ × Q
are transitions, and Γ ⊆ Q × Σ × Q is the transition-based acceptance condition.
A run r of A on w ∈ Σ
ω is an ω-word r 0 , w 0 , r 1 , w 1 , . . . in (Q×Σ)
ω such that r 0 =
q 0 and, for i > 0, it is (r i−1 , w i−1 , r i ) ∈ Δ. We write inf(r) for the set of transitions
that appear infinitely often in the run r. A run r of A is accepting if inf(r) ∩ Γ = ∅.
The language, L A , of A (or, recognized by A) is the subset of words in Σ
ω that have
accepting runs in A. A language is ω-regular if it is accepted by a B¨ uchi automaton. An
automaton A = Σ, Q, Q 0 , Δ, Γ is deterministic if (q, σ, q
), (q, σ, q
) ∈ Δ implies
q
= q
. A is complete if, for all σ ∈ Σ and all q ∈ Q, there is a transition (q, σ, q
) ∈
Δ. A word in Σ
ω has exactly one run in a deterministic, complete automaton.
A Markov decision process (MDP) M is a tuple (S, A, T, Σ, L) where S is a finite
set of states, A is a finite set of actions, T : S × A − D(S), where D(S) is the set of
probability distributions over S, is the probabilistic transition (partial) function, Σ is