On Good-for-MDPs Automata
Sven Schewe, Qiyi Tang, Tansholpan Zhanabekova

TL;DR
This paper introduces a decision procedure for checking if automata are good-for-MDPs (GFM), compares GFM automata's succinctness with other automata classes, and establishes exponential gaps in their sizes.
Contribution
It proves that GFM automata are decidable with an EXPTIME procedure, and characterizes the exponential size gaps between GFM, GFG, and nondeterministic automata.
Findings
GFM-ness is decidable in EXPTIME.
GFM automata are exponentially more succinct than GFG automata.
The exponential size gap persists even for restricted automata classes.
Abstract
Nondeterministic good-for-MDPs (GFM) automata are for MDP model checking and reinforcement learning what good-for-games (GFG) automata are for reactive synthesis: a more compact alternative to deterministic automata that displays nondeterminism, but only so much that it can be resolved locally, such that a syntactic product can be analysed. GFM has recently been introduced as a property for reinforcement learning, where the simpler B\"uchi acceptance conditions it allows to use is key. However, while there are classic and novel techniques to obtain automata that are GFM, there has not been a decision procedure for checking whether or not an automaton is GFM. We show that GFM-ness is decidable and provide an EXPTIME decision procedure as well as a PSPACE-hardness proof. We also compare the succinctness of GFM automata with other types of automata with restricted nondeterminism. The…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
