2026-07-21T12:46:38Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:19029 2024-03-06T11:03:19Z ddc:004 open_access

Deciding What Is Good-For-MDPs Schewe, Sven Tang, Qiyi Zhanabekova, Tansholpan Büchi automata Markov Decision Processes Omega-regular objectives Reinforcement learning Nondeterministic good-for-MDPs (GFM) automata are for MDP model checking and reinforcement learning what good-for-games 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üchi 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Sven Schewe and Qiyi Tang and Tansholpan Zhanabekova 2023 Is Part Of LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2023.35 urn:nbn:de:0030-drops-190290 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.35 eng https://creativecommons.org/licenses/by/4.0/legalcode