Good-for-MDPs Automata for Probabilistic Analysis
and Reinforcement Learning
Ernst Moritz Hahn
1,2 , Mateo Perez
3 ,
Sven Schewe
4 , Fabio Somenzi
3 ,
Ashutosh Trivedi
3 , and Dominik Wojtczak
4
1 School of EEECS, Queen’s University Belfast, UK
2 State Key Laboratory of Computer Science, Institute of Software, CAS, PRC
3 University of Colorado Boulder, USA
4 University of Liverpool, UK
Abstract. We characterize the class of nondeterministic ω-automata that can be
used for the analysis of finite Markov decision processes (MDPs). We call these
automata ‘good-for-MDPs’ (GFM). We show that GFM automata are closed under classic simulation as well as under more powerful simulation relations that
leverage properties of optimal control strategies for MDPs. This closure enables
us to exploit state-space reduction techniques, such as those based on direct and
delayed simulation, that guarantee simulation equivalence. We demonstrate the
promise of GFM automata by defining a new class of automata with favorable
properties—they are B¨ uchi automata with low branching degree obtained through
a simple construction—and show that going beyond limit-deterministic automata
may significantly benefit reinforcement learning.
1 Introduction
System specifications are often captured in the form of finite automata over infinite
words (ω-automata), which are then used for model checking, synthesis, and learning. Of the commonly-used types of ω-automata, B¨ uchi automata have the simplest
acceptance condition, but require nondeterminism to recognize all ω-regular languages.
Nondeterministic machines can use unbounded look-ahead to resolve nondeterministic
choices. However, important applications—like reactive synthesis or model checking
and reinforcement learning (RL) for Markov Decision Process (MDPs [23])—have a
game setting, which restrict the resolution of nondeterminism to be based on the past.
Being forced to resolve nondeterminism on the fly, an automaton may end up rejecting words it should accept, so that using it can lead to incorrect results. Due to this difficulty, initial solutions to these problems have been based on deterministic automata—
usually with Rabin or parity acceptance conditions. For two-player games, Henzinger
and Piterman proposed the notion of good-for-games (GFG) automata [15]. These are
nondeterministic automata that simulate [21,14,9] a deterministic automaton that recognizes the same language. The existence of a simulation strategy means that nondeterministic choices can be resolved without look-ahead.
This work has been supported by the National Natural Science Foundation of China (Grant Nr.
61532019), EPSRC grants EP/M027287/1 and EP/P020909/1, and a CU Boulder RIO grant.
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 306–323, 2020.
https://doi.org/10.1007/978-3-030-45190-5 17
TACAS
Evaluation
Artifact
2020
Accepted
and Reinforcement Learning
Ernst Moritz Hahn
1,2 , Mateo Perez
3 ,
Sven Schewe
4 , Fabio Somenzi
3 ,
Ashutosh Trivedi
3 , and Dominik Wojtczak
4
1 School of EEECS, Queen’s University Belfast, UK
2 State Key Laboratory of Computer Science, Institute of Software, CAS, PRC
3 University of Colorado Boulder, USA
4 University of Liverpool, UK
Abstract. We characterize the class of nondeterministic ω-automata that can be
used for the analysis of finite Markov decision processes (MDPs). We call these
automata ‘good-for-MDPs’ (GFM). We show that GFM automata are closed under classic simulation as well as under more powerful simulation relations that
leverage properties of optimal control strategies for MDPs. This closure enables
us to exploit state-space reduction techniques, such as those based on direct and
delayed simulation, that guarantee simulation equivalence. We demonstrate the
promise of GFM automata by defining a new class of automata with favorable
properties—they are B¨ uchi automata with low branching degree obtained through
a simple construction—and show that going beyond limit-deterministic automata
may significantly benefit reinforcement learning.
1 Introduction
System specifications are often captured in the form of finite automata over infinite
words (ω-automata), which are then used for model checking, synthesis, and learning. Of the commonly-used types of ω-automata, B¨ uchi automata have the simplest
acceptance condition, but require nondeterminism to recognize all ω-regular languages.
Nondeterministic machines can use unbounded look-ahead to resolve nondeterministic
choices. However, important applications—like reactive synthesis or model checking
and reinforcement learning (RL) for Markov Decision Process (MDPs [23])—have a
game setting, which restrict the resolution of nondeterminism to be based on the past.
Being forced to resolve nondeterminism on the fly, an automaton may end up rejecting words it should accept, so that using it can lead to incorrect results. Due to this difficulty, initial solutions to these problems have been based on deterministic automata—
usually with Rabin or parity acceptance conditions. For two-player games, Henzinger
and Piterman proposed the notion of good-for-games (GFG) automata [15]. These are
nondeterministic automata that simulate [21,14,9] a deterministic automaton that recognizes the same language. The existence of a simulation strategy means that nondeterministic choices can be resolved without look-ahead.
This work has been supported by the National Natural Science Foundation of China (Grant Nr.
61532019), EPSRC grants EP/M027287/1 and EP/P020909/1, and a CU Boulder RIO grant.
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 306–323, 2020.
https://doi.org/10.1007/978-3-030-45190-5 17
TACAS
Evaluation
Artifact
2020
Accepted