Automated Technology for Verification and Analysis - 20th International Symposium, ATVA 2022, Virtual Event, October 25-28, 2022, Proceedings
Automated Technology for Verification and Analysis - 20th International Symposium, ATVA 2022, Virtual Event, October 25-28, 2022, Proceedings
复制标题
验证和分析自动化技术 - 第 20 届国际研讨会，ATVA 2022，虚拟活动，2022 年 10 月 25-28 日，会议记录
DOI：
10.1007/978-3-031-19992-9_19
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Hahn E
中科院分区：
文献类型：
--
作者：
Hahn E
当ω正则目标首次在无模型强化学习（RL）中被提出用于控制MDP时，确定性Rabin自动机被用来试图提供从它们的转换到标量值的直接转换。虽然这些翻译失败了，但事实证明可以通过使用Good-for-MDP（GFM）Büchi自动机来修复它们。这些都是非确定性的Büchi自动机，具有受限类型的非确定性，尽管不像游戏自动机那样受限。事实上，确定性拉宾自动机有一个相当直接的翻译，这样的GFM自动机，这是双线性的状态和对的数量。有趣的是，对于确定性Streett自动机来说，情况并非如此：即使不要求目标自动机是好的MDP，向非确定性Rabin或Büchi自动机的转换也会以指数级代价进行。我们是否必须支付更多的钱来获得一个好的MDP自动机？令人惊讶的答案是，当我们将good-for-MDP属性扩展到交替自动机时，我们必须付出更少的代价：就像从确定性Rabin自动机获得的非确定性GFM自动机一样，我们从确定性Streett自动机产生的交替good-for-MDP自动机在确定性自动机及其索引的大小上是双线性的。因此，它们可以比最小不确定Büchi自动机以指数级方式更加简洁。
When omega-regular objectives were first proposed in model-free reinforcement learning (RL) for controlling MDPs, deterministic Rabin automata were used in an attempt to provide a direct translation from their transitions to scalar values. While these translations failed, it has turned out that it is possible to repair them by using good-for-MDPs (GFM) Büchi automata instead. These are nondeterministic Büchi automata with a restricted type of nondeterminism, albeit not as restricted as in good-for-games automata. Indeed, deterministic Rabin automata have a pretty straightforward translation to such GFM automata, which is bi-linear in the number of states and pairs. Interestingly, the same cannot be said for deterministic Streett automata: a translation to nondeterministic Rabin or Büchi automata comes at an exponential cost, even without requiring the target automaton to be good-for-MDPs. Do we have to pay more than that to obtain a good-for-MDPs automaton? The surprising answer is that we have to pay significantly less when we instead expand the good-for-MDPs property to alternating automata: like the nondeterministic GFM automata obtained from deterministic Rabin automata, the alternating good-for-MDPs automata we produce from deterministic Streett automata are bi-linear in the size of the deterministic automaton and its index. They can therefore be exponentially more succinct than the minimal nondeterministic Büchi automaton.