Good-for-MDPs Automata
321
a0
a1
a2
x
y
x
y
¬y
q0
q1
q2
y
¬y
x ∧ ¬y
x ∧ ¬y
y
¬x ∧ ¬y
¬y
y
Fig. 5. Two GFM automata for (F G x) ∨ (G F y). SLDBA (left), and forgiving (right)
Fig. 6. Learning curves
Training of the continuous-statespace
model employed PPO [28] as implemented in OpenAI Baselines [6]. Figure 6 shows the learning curves for the
three automata averaged over ten runs.
They underline the importance of choosing the right automaton in RL. Training
parameters, more details on the model,
and additional examples can be found in
the extended version of this paper [13].
6 Conclusion
We have defined the class of automata that are good for MDPs—nondeterministic automata that can be used for the analysis of MDPs—and shown it to be closed under
different simulation relations. This has multiple favorable implications for model checking and reinforcement learning. Closure under classic simulation opens a rich toolbox
of statespace reduction techniques that come in handy to push the boundary of analysis
techniques, while the more powerful (and more expensive) AEC simulation has promise
to identify source automata that happen to be good for MDPs.
The wider class of GFM automata also shows promise: the slim automata we have
defined to tame the branching degree while retaining the desirable B¨ uchi condition for
reinforcement learning are able to compete even against optimized SLDBAs.
As outlined in Section 5.2, a low branching degree, cautiousness, and forgiveness
make automata particularly well-suited for learning. From a practical point of view,
much of the power of this new approach is in harnessing the power of simulation for
learning, and forgiveness is closely related to simulation.
The natural follow-up research is to tap the full potential of simulation-based statespace reduction instead of the limited version that we have implemented. Besides using
this to get the statespace small—useful for model checking—we will use simulation to
construct forgiving automata, which is promising for reinforcement learning.
Datasets generated and analyzed during the current study are available at:
https://doi.org/10.6084/m9.figshare.11882739 [35,36]
321
a0
a1
a2
x
y
x
y
¬y
q0
q1
q2
y
¬y
x ∧ ¬y
x ∧ ¬y
y
¬x ∧ ¬y
¬y
y
Fig. 5. Two GFM automata for (F G x) ∨ (G F y). SLDBA (left), and forgiving (right)
Fig. 6. Learning curves
Training of the continuous-statespace
model employed PPO [28] as implemented in OpenAI Baselines [6]. Figure 6 shows the learning curves for the
three automata averaged over ten runs.
They underline the importance of choosing the right automaton in RL. Training
parameters, more details on the model,
and additional examples can be found in
the extended version of this paper [13].
6 Conclusion
We have defined the class of automata that are good for MDPs—nondeterministic automata that can be used for the analysis of MDPs—and shown it to be closed under
different simulation relations. This has multiple favorable implications for model checking and reinforcement learning. Closure under classic simulation opens a rich toolbox
of statespace reduction techniques that come in handy to push the boundary of analysis
techniques, while the more powerful (and more expensive) AEC simulation has promise
to identify source automata that happen to be good for MDPs.
The wider class of GFM automata also shows promise: the slim automata we have
defined to tame the branching degree while retaining the desirable B¨ uchi condition for
reinforcement learning are able to compete even against optimized SLDBAs.
As outlined in Section 5.2, a low branching degree, cautiousness, and forgiveness
make automata particularly well-suited for learning. From a practical point of view,
much of the power of this new approach is in harnessing the power of simulation for
learning, and forgiveness is closely related to simulation.
The natural follow-up research is to tap the full potential of simulation-based statespace reduction instead of the limited version that we have implemented. Besides using
this to get the statespace small—useful for model checking—we will use simulation to
construct forgiving automata, which is promising for reinforcement learning.
Datasets generated and analyzed during the current study are available at:
https://doi.org/10.6084/m9.figshare.11882739 [35,36]