Good-for-MDPs Automata
307
The situation is better in the case of probabilistic model checking, because the game
for which a strategy is sought is played on an MDP against “blind nature,” rather than
against a strategic opponent who may take advantage of the automaton’s inability to
resolve nondeterminism on the fly. As early as 1985, Vardi noted that probabilistic
model checking can be performed with B¨ uchi automata endowed with a limited form
of nondeterminism [34]. Limit deterministic B¨ uchi automata (LDBA) [4,11,29] perform
no nondeterministic choice after seeing an accepting transition. Still, they recognize
all ω-regular languages and are, under mild restrictions [29], suitable for probabilistic
model checking.
Related Work. The production of deterministic and limit deterministic automata for
model checking has been intensively studied [24,22,1,26,33,32,27,29,8,30,20], and several tools are available to produce different types of automata, incl. MoChiBA/Owl
[29,30,20], LTL3BA [1], GOAL [33,32], SPOT [8], Rabinizer [19], and B¨ uchifier [16].
So far, only deterministic and a (slightly restricted [29]) class of limit deterministic automata have been considered for probabilistic model checking [34,4,11,29].
Thus, while there have been advances in the efficient production of such automata
[11,29,30,20], the consideration of suitable LDBAs by Courcoubetis and Yannakakis
in 1988 [3] has been the last time when a fundamental change in the automata foundation of MDP model checking has occurred.
Contribution. The simple but effective observation that simulation preserves the suitability for MDPs (for both traditional simulation and the AEC simulation we introduce)
extends the class of automata that can be used in the analysis of MDPs. This provides us
with three advantages: The first advantage is that we can now use a wealth of simulation
based statespace reduction techniques [7,31,10,9] on an automaton A (e.g. an SLDBA)
that we would otherwise use for MDP model checking. The second advantage is that
we can use A to check if a different language equivalent automaton, such as an NBA
B (e.g. an NBA from which A is derived) simulates A. For this second advantage, we
can dip into the more powerful class of AEC simulation we define in Section 4 that use
properties of winning strategies on finite MDPs. While this is not a complete method
for identifying GFM automata, our experimental results indicate that the GFM property
is quite frequent for NBAs constructed from random formulas, and can often be established efficiently, while providing a significant statespace reduction and thus offering a
significant advantage for model checking.
A third advantage is that we can use the additional flexibility to tailor automata
for different applications than model checking, for which specialized automata classes
have not yet been developed. We demonstrate this for model-free reinforcement learning (RL). We argue that RL benefits from three properties that are less important in
model checking: The first—easy to measure—property is a small number of successors, the second and third, are cautiousness, the scope for making wrong decisions, and
forgiveness, the resilience against making wrong decisions, respectively.
A small number of successors is a simple and natural goal for RL, as the lack of
an explicit model means that the product space of a model and an automaton cannot
be evaluated backwards. In a forward analysis, it matters that nondeterministic choices
have to be modeled by enriching the decisions in the MDPs with the choices made
by the automaton. For LDBAs constructed from NBAs, this means guessing a suit-
307
The situation is better in the case of probabilistic model checking, because the game
for which a strategy is sought is played on an MDP against “blind nature,” rather than
against a strategic opponent who may take advantage of the automaton’s inability to
resolve nondeterminism on the fly. As early as 1985, Vardi noted that probabilistic
model checking can be performed with B¨ uchi automata endowed with a limited form
of nondeterminism [34]. Limit deterministic B¨ uchi automata (LDBA) [4,11,29] perform
no nondeterministic choice after seeing an accepting transition. Still, they recognize
all ω-regular languages and are, under mild restrictions [29], suitable for probabilistic
model checking.
Related Work. The production of deterministic and limit deterministic automata for
model checking has been intensively studied [24,22,1,26,33,32,27,29,8,30,20], and several tools are available to produce different types of automata, incl. MoChiBA/Owl
[29,30,20], LTL3BA [1], GOAL [33,32], SPOT [8], Rabinizer [19], and B¨ uchifier [16].
So far, only deterministic and a (slightly restricted [29]) class of limit deterministic automata have been considered for probabilistic model checking [34,4,11,29].
Thus, while there have been advances in the efficient production of such automata
[11,29,30,20], the consideration of suitable LDBAs by Courcoubetis and Yannakakis
in 1988 [3] has been the last time when a fundamental change in the automata foundation of MDP model checking has occurred.
Contribution. The simple but effective observation that simulation preserves the suitability for MDPs (for both traditional simulation and the AEC simulation we introduce)
extends the class of automata that can be used in the analysis of MDPs. This provides us
with three advantages: The first advantage is that we can now use a wealth of simulation
based statespace reduction techniques [7,31,10,9] on an automaton A (e.g. an SLDBA)
that we would otherwise use for MDP model checking. The second advantage is that
we can use A to check if a different language equivalent automaton, such as an NBA
B (e.g. an NBA from which A is derived) simulates A. For this second advantage, we
can dip into the more powerful class of AEC simulation we define in Section 4 that use
properties of winning strategies on finite MDPs. While this is not a complete method
for identifying GFM automata, our experimental results indicate that the GFM property
is quite frequent for NBAs constructed from random formulas, and can often be established efficiently, while providing a significant statespace reduction and thus offering a
significant advantage for model checking.
A third advantage is that we can use the additional flexibility to tailor automata
for different applications than model checking, for which specialized automata classes
have not yet been developed. We demonstrate this for model-free reinforcement learning (RL). We argue that RL benefits from three properties that are less important in
model checking: The first—easy to measure—property is a small number of successors, the second and third, are cautiousness, the scope for making wrong decisions, and
forgiveness, the resilience against making wrong decisions, respectively.
A small number of successors is a simple and natural goal for RL, as the lack of
an explicit model means that the product space of a model and an automaton cannot
be evaluated backwards. In a forward analysis, it matters that nondeterministic choices
have to be modeled by enriching the decisions in the MDPs with the choices made
by the automaton. For LDBAs constructed from NBAs, this means guessing a suit-